Assignment 3 - SVF-tools/Teaching-Software-Verification GitHub Wiki

Assignment-3 folder layout

$tree Assignment-3
├── Assignment-3.cpp
├── Assignment-3.h
├── CMakeLists.txt
├── Test3.cpp

$tree python
├── Assignment-3
   └── Assignment-3.py

Make sure to switch your program to assign-3 before coding. For python user, you can set "program": "${workspaceFolder}/python/Assignment-3/Assignment-3.py" in launch.json.

1. Assignment 3 task

Implement methods from Z3Examples::test1() to Z3Examples::test10() in class Z3Examples in Assignment-3.cpp. Or for Python user, impelment methods from Z3Mgr.test1() to Z3Mgr.test10() in Assignment-3.py
Pass the test without any assertion by Test3.cpp. For Python user, pass the tests in the __main__ function.
Submit Assignment-3.cpp or Assignment-3.py 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. We have provided Z3ExampleMgr::test0() in Test3.cpp or Assignment-3.py as an example to help get started.

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

SVF Z3Mgr APIs to help with your implementation SVF Z3Mgr API or SVF Z3Mgr Python API

2. visualize ICFG and Debugging

Visualize ICFG by following here