Skip to main content Link Menu Expand (external link) Document Search Copy Copied

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.


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


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.


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.


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.