Deadline: March 11, 2012 (midnight), that is, you have one week.

Homework 02 - Relations

Please type up your solution and submit it through Moodle.
The solution of Exercise 2 and a partial solution for Exercise 4 from Lab 2 are available from the lab's wiki. They should give you an idea about how detailed your proofs should be, and maybe help with some of the homework questions.

You should first update your repository with the files contained in this archive. You will then have a working parser for a subset of scala. The parser generates abstract syntax trees. Please have a look at the files in the test/ directory to see what you can do in the language.

The file cfg/CFG.scala defines classes used to represent control flow graphs. A control flow graph is an intermediate representation of a program that is simpler than the abstract syntax tree. Each node in the graph represents a program point and the edges of the graph represent transitions between program points. The transitions are label with assume, assign, or havoc statements. If statements and while loops give rise to branching and loops in the CFG. We will base our future code analysis on control flow graphs.

Your task is to complete MakeCFG.scala in order to generate a control flow graph from the Abstract Syntax Tree of a method's body.

You should assume that the ASTs that your code will receive contain no function declarations, no object creation, and no function calls. Note that assume, assert, and havoc are parsed as function calls to functions named sc_assume, sc_assert, and sc_havoc. For asserts, you should create a special CFG vertex that represents errors and that is reached if any assert fails. We included a control flow graph viewer that you can use to check the output of your code.