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

$tree python/Assignment-4 ├── Assignment-4.py └── 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

Make sure to [switch your program to `assign-4`](https://github.com/SVF-tools/Teaching-Software-Verification/blob/main/.vscode/launch.json#L8) and make a [testcase bc](https://github.com/SVF-tools/Teaching-Software-Verification/tree/main/Assignment-4/testcase/bc) as the [input argument](https://github.com/SVF-tools/Teaching-Software-Verification/blob/main/.vscode/launch.json#L9) before running your implementation.

## 1. Assignment 4 task
1. Implement `TODO` methods of class [`SSE`](https://github.com/SVF-tools/Teaching-Software-Verification/blob/main/Assignment-4/Assignment-4.cpp), which is a subclass of [`ICFGTraversal'](https://github.com/SVF-tools/Teaching-Software-Verification/blob/main/Assignment-2/Assignment-2.h). 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. Put your previously implemented Assignment-2.cpp in place (under the Assignment-2 folder).
3. Pass the three tests without any assertion by the driver program [`Test4.cpp`](https://github.com/SVF-tools/Teaching-Software-Verification/blob/main/Assignment-4/Test4.cpp). 
4. 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](https://github.com/SVF-tools/Teaching-Software-Verification/wiki/Z3-API).

## 2. visualize ICFG and Debugging
Visualize ICFG by following [here](https://github.com/SVF-tools/Teaching-Software-Verification/wiki/SVFIR#4-visualize-icfg-and-pag)

You can debug by printing all the values of all expressions using `printExprValues()` method in [`Z3SSEMgr`](https://github.com/SVF-tools/Teaching-Software-Verification/blob/main/Z3Manager/Z3Mgr.h) class.