Skip to content

Assignment 3

Xiao edited this page Feb 12, 2025 · 5 revisions

Assignment-3 folder layout

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

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

1. Assignment 3 task

  1. Implement methods from Z3ExampleMgr::test1() to Z3ExampleMgr::test7() in class Z3ExampleMgr in Assignment-3.cpp
  2. Pass the test without any assertion by Test3.cpp.
  3. Submit Assignment-3.cpp to canvas. Your implementation will be evaluated against our 7 internal tests. You will get the full marks if your code can pass them all. We have provided Z3ExampleMgr::test0() in Test3.cpp 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.

2. visualize ICFG and Debugging

Visualize ICFG by following here

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

Clone this wiki locally