Assignment 4

Assignment-4 folder layout

$tree Assignment-4
├── Assignment-4.cpp
├── Assignment-4.h
├── CMakeLists.txt
├── Test4.cpp
└── testcase
    ├── bc
    │   ├── test1.ll
    │   └── test2.ll
    │   └── test3.ll
    ├── dot
    │   ├── icfg_test1.dot
    │   └── icfg_test2.dot
    │   └── icfg_test3.dot
    └── src
        ├── test1.c
        └── test2.c
        └── test3.c

1. Get the latest assignment-4 code template

* Before coding, please type cd $HOME/Teaching-Software-Verification and git pull in your terminal to make sure you always have the latest version of the code template before each assignment.

If git pull fails due to the conflict with your local changes, type git stash to store your current code in a temporal branch and type git pull again. If you want to retrieve your code back, type git stash pop.

Make sure to switch your program to assign-4 before coding.

2. Assignment 4 task

1. Implement SSE::handleCall, SSE::handleRet, SSE::handleBranch and SSE::handleNonBranch methods of class SSE, which is a subclass of `ICFGTraversal'. The required implementation parts are indicated with TODO comments and you only need to fill up the code template if a method is partially implemented.
2. Pass the three tests without any assertion by the driver program Test4.cpp.
3. Submit Assignment-4.cpp to canvas. Your implementation will be evaluated against our 10 internal tests. You will get the full marks if your code can pass them all. Unfortunately, our internal tests are publicly available. Here, we only provided three test cases in the folder testcase. You are encouraged to add more test cases by yourself to validate the correctness of your implementation.

*You will be working on Assignment-4.cpp only and there is NO need to modify other files under the Assignment-4 folder

SVF Z3Mgr APIs to help with your implementation SVF Z3Mgr API.

3. visualize ICFG and Debugging

Visualize ICFG by following here

You can debug by printing all the values of all expressions using printExprValues() method in Z3SSEMgr class.