15-122 Principles of Imperative Computation
Recitation 1 - Wed Jan 12

Navigating your account in Linux
Editing your program
Compiling your program
Running your program
Accessing your Andrew files using ssh

Navigating your account in Linux

Open up a Terminal window to access the Linux command prompt. (Unlike typical graphical interfaces for operating systems, here you are entering commands directly to the OS and can change hundreds of options to give finer control of what you're doing.) On the Linux machines in the computer labs in Gates (rooms 5205, 5201, and 3000), you can access a Terminal window using the Applications --> Accessories menus.

In the Gates computer labs, your terminal window will give you a prompt and you will be in your home directory in your Andrew account. Type ls (to list files) to see what files and directories are there. Back in the day, we used to call folders "directories". To move to another directory, use the cd command (for "change directory"):

cd private

ACADEMIC INTEGRITY NOTE: You should store your program files inside the private directory (or a subdirectory inside this directory) since this directory is automatically set to prevent viewing by other users. Remember that you should protect your code from being viewed by other students as part of the academic integrity policy for this course.

Since you will write a number of programs for this course, it pays to make a subdirectory inside the private directory. Once you cd into the private directory, make a new directory named 15122:

mkdir 15122

Now go into this directory using cd again:

cd 15122

To go back up one directory if you need to, use this command:

cd ..

You can go up two directories and down another directory (e.g. public) like this:

cd ../../public

If you ever get lost while you change from one directory to another, you can use pwd to find your present working directory. Or if you want to go back to your home directory, simple type:


You can also access any directory from your home directory using the shell variable $HOME or the "tilde" character ~. For example, you can get to your 15122 directory from any directory on Andrew by typing this:

cd $HOME/private/15122

or this:

cd ~/private/15122

LOGGING OUT: Remember that you must log out from the computer in the Gates lab. Closing the terminal window is not enough! To log out, go to the System menu and choose Log Out. You don't want others accessing your account if you leave yourself logged in.

COURTESY NOTE: In the Gates labs, if you don't use your lab computer for a set period of time, the screen saver will launch and you can't access the terminal unless you type your password in. Some students have left the computer this way so they can "reserve" the machine for themselves later. If we find a machine in screen saver mode and no user at that terminal, we will automatically log you out so you may lose work if you're not careful. Please be considerate of others and don't lock the terminal.


Computing Services - Unix Help Page

Editing your program

You can use any editor you wish to write and edit your programs but we highly recommend you try out emacs since this editor can do much more than just help you edit your code (as you will see).

To set up emacs for your Andrew account, you will need to create a configuration file named .emacs in your home directory. Run the following configure command located in the course directory and redirect the output into the .emacs file:

/afs/andrew/course/15/122/c0-mode/configure > ~/.emacs

When you want to edit a program now, you can enter emacs specifying the file name you want to edit. You should be in the directory where the file is or should be (to keep things simple for now). For example, to open the file test.c0 in emacs, you'd go to the directory where this file should be stored and enter:

emacs test.c0

If the file exists, it will be loaded into the emacs editor. If the file does not exist, you will get a blank editor to start typing in the code. The configuration file .emacs you edited earlier will add color coding to your c0 programs. Keywords will show up in one color, variables in another, etc. This will make it easier to edit your program code.


LinuxHelp.next Emacs Help

Compiling your program

Before you compile programs, you should update your path in your Andrew account so the system can find the C0 compiler without you having to explicitly give the full path to the compiler's location.

To update your path, use emacs to edit the file .cshrc found in your home directory when you log in:

emacs .cshrc

Add the following line at the end of your .cshrc file exactly as shown:

setenv PATH ${PATH}:/afs/andrew/course/15/122/bin

Save the file and exit emacs. For this time only, you can have the system run this resource file immediately by entering the following at the Linux prompt in your terminal window:

source .cshrc

(When you log in next time, this file is "sourced" automatically.) If you use a different shell than csh, you will need to adjust your path accordingly. See your TA or CA if you need more help.

Now to compile your code, go to the directory that contains your C0 code and type:

cc0 filename.c0

If your code compiles without syntax errors, then you will just get the Linux prompt back. If there are syntax errors, you will get one or more (ugly) messages. The key here is to look at the first message for the line number where things started to go wrong. For example, here is a sample error message:

test.c0:11.8-11.12:error:syntax error: deleting LBRACKET RBRACKET EQ

This message indicates that there was a syntax error on line 11 starting at character 8 to line 11 at character 12. You can go back into emacs (or your favorite editor) to find and correct the error. Note that if you have a syntax error, you may get a number of additional error messages since the compiler is trying to "delete" some of your code to see if the rest of your code has other errors. This will likely cause more errors to be generated! So focus on the first error and hopefully the others will start disappearing when you recompile.

As you saw in class, you should have annotations (contracts) in your code to describe various assertions, invariants, etc. If you want to have these checked as well when you run your program ("dynamic checking"), compile your program using the -d switch/flag:

cc0 -d filename.c0

If your program has more than one file, simply list the files one at a time on the command line when you compile (with dynamic checking if desired):

cc0 -d filename1.c0 filename2.c0 filename3.c0

To find out more options for the compiler, you can just type cc0 at the Linux prompt, and you should see something like this:

Usage: /afs/andrew/course/15/122/bin/cc0 [OPTION...] SOURCEFILE
where OPTION is
  -v         --verbose        Give verbose status and error messages
  -h         --help           Give short usage message and exit
             --dump-ast       Pretty print the program's abstract syntax tree
  -d         --dyn-check      Check contracts dynamically
  -s         --save-files     Save the .c and .h files produced by the compiler
  -x         --exec           Execute compiled file
  -o <file>  --output=<file>  Place the executable output into <file>
  -l <lib>   --library=<lib>  Include the library <lib>
  -L <dir>                    Add <dir> to the search path for libraries
  -r dir     --runtime=dir    Select a runtime (default "bare")

Running Your Program

Once your program compiles without syntax errors, it will generate an executable file in the same directory named a.out. To run this program, type:


This command says to look in the current directory (.) and run a.out. Normally the system doesn't look in the current directory for executable programs unless you have "." in your PATH.

If you compiled your program with the -d option, then your program will run and all contracts/annotations will be checked during runtime. Examine your output for runtime and logical errors and for contract violations. If you have any, go back to edit your code again with emacs, save the file, recompile and run again.

In some cases, when you run your program, you will need to specify additional command line options (similar to when you compiled your program). Look for further instructions in these cases.

Accessing your Andrew files using ssh

You can always access your Andrew files on the Andrew Linux server in the Gates labs (rooms 5205, 5201, and 3000) when the labs have no classes scheduled. In addition, you can access your files via ssh in several ways. ssh (secure shell) a protocol for securely logging into remote servers like the Andrew system.

Windows machines: Download a free ssh client like PuTTY. When you log in, specify the server linux.andrew.cmu.edu.

In the Windows clusters on campus, you should run X-Win32 first and then use an SSH client like SSH Tectia-Terminal to log in to linux.andrew.cmu.edu. By having the X-Win32 program running, all "windows" that you open up when logged into andrew (e.g. when you run emacs) will appear on your local Windows console.

Mac and Linux machines: Open up a terminal window and run this command:

ssh -l yourusername linux.andrew.cmu.edu

and enter your password when prompted to log in. (Your machine might ask if you want to add the server to a list of known hosts; if so, answer yes.)


Using emacs, type in the following simple C0 program:

int main() {
    return 0;

The main function returns an integer (0) so we need to specify the return type int. Save this file and exit emacs. Compile it:

cc0 test.c0

and then run it (if there are no syntax errors):

and you should see the value 0 which is returned from main.

Now, use emacs to edit the file again:

emacs test.c0

and enter the following program:

int area(int width, int height)
    return width * height;
int main() {
    return area(15, 122);

Save this file and exit emacs. This program returns the area of a rectangle that has a width of 15 and height of 122. Compile and run it. You should get the output 1830 as the computed area. Now go back into emacs and edit the file, changing 15 to -15:

int area(int width, int height)
    return width * height;
int main() {
    return area(-15, 122);

Now this doesn't make sense since a rectangle can't have a width of -15. But if you compile and run this, you get an answer that doesn't make sense. (You can't have an area that is -1830.) We only want to compute the area if both width and height are positive. So we can add a C0 annotation to require this. Use emacs to make the following edits:

int area(int width, int height)
//@requires width > 0;
//@requires height > 0;
    return width * height;
int main() {
    return area(-15, 122);

If you compile and run this as before, it still produces the same negative output, since the annotations will be treated as comments by default. But you can use the -d flag when you compile to turn on dynamic checking:

cc0 -d test.c0

Now when you run the program, the c0 annotations are also executed. In this case, we get an annotation violation since width is not positive:

test.c0:2.4-2.23: @requires annotation failed

The error message indicates that the requires annotation on line 2 failed so width was not positive. As you will see in class, we will use annotations to help us state what the code is supposed to be doing, and we will use dynamic checking to make sure the code is doing what we intend as it executes.

written by Tom Cortina, 1/12/11