-
Notifications
You must be signed in to change notification settings - Fork 23
Z3 API
guanqin-123 edited this page Apr 12, 2022
·
27 revisions
We describe Z3Mgr and its subclasses Z3ExampleMgr and Z3SSEMgr for implementing Assignment-3 and Assignment-4.
| Members | Meanings |
|---|---|
| SVF:: Z3Mgr::resetZ3ExprMap | reset added expressions and clean all declared values |
| SVF:: Z3Mgr::storeValue(const z3::expr loc, const z3::expr value) | store expr(value) to expr(loc), which is used for store instructions |
| SVF:: Z3Mgr::loadValue(const z3::expr loc) | retrieve the expression from expr(loc) |
| SVF:: Z3Mgr::getZ3Expr(u32_t idx) | return Z3 expression based on SVFVar ID |
| SVF:: Z3Mgr::updateZ3Expr(u32_t idx, z3::expr target) | update expression when assignments |
| SVF:: Z3Mgr::getEvalExpr(z3::expr e) | return int value from an expression if it is a numeral, otherwise return an approximate value |
| SVF:: Z3Mgr::getSolver | return the Z3's solver |
| SVF:: Z3Mgr::getCtx | return the Z3's context |
| Members | Meanings |
|---|---|
| SVF:: Z3SSEMgr:: createExprForValVar(const ValVar* val) | declare the expr type for each top-level pointers |
| SVF:: Z3SSEMgr:: createExprForObjVar(const ObjVar* obj) | initialize the expr value for each objects (address-taken variables and constants) |
| SVF:: Z3SSEMgr::getMemObjAddress(u32_t idx) | return the address expr of a ObjVar |
| SVF:: Z3SSEMgr::getGepObjAddress(z3::expr pointer, u32_t offset) | return the field address given a pointer points to a struct object and an offset |
| SVF:: Z3SSEMgr::getGepOffset(const GepStmt* gep) | return the offset expression of a GepStmt |
| SVF:: Z3SSEMgr:: printExprValues | dump values of all added expressions in the solver |