Building Pintos

You can build Pintos by running make in the directory appropriate for the project you are working on (ie. userprog/, threads/, or filesys/). This section describes the interesting files inside the build directory, which appears when you run make as above.

build/Makefile

A copy of Makefile.build. Don’t change this file, because your changes will be overwritten if you run make clean and re-compile. Make your changes to Makefile.build instead. For more information, see Adding Source Files.

build/kernel.o

Object file for the entire kernel. This is the result of linking object files compiled from each individual kernel source file into a single object file. It contains debug information, so you can run GDB or backtrace on it.

build/kernel.bin

Memory image of the kernel, that is, the exact bytes loaded into memory to run the Pintos kernel. This is just kernel.o with debug information stripped out, which saves a lot of space, which in turn keeps the kernel from bumping up against a 512 kB size limit imposed by the kernel loader’s design.

build/loader.bin

Memory image for the kernel loader, a small chunk of code written in assembly language that reads the kernel from disk into memory and starts it up. It is exactly 512 bytes long, a size fixed by the PC BIOS.

Subdirectories of build/ contain object files (*.o) and dependency files (*.d), both produced by the compiler. The dependency files tell make which source files need to be recompiled when other source or header files are changed.