SVF Python Z3 API - SVF-tools/Software-Security-Analysis GitHub Wiki

Z3Mgr API Documentation

Method	Description
`getZ3Expr(var_id: int, ctx)`	Retrieves the Z3 expression for a given variable ID within a context.
`getZ3Val(value)`	Converts a value to a Z3 value.
`addToSolver(expr)`	Adds an expression to the Z3 solver.
`solver.push()`	Pushes a context onto the solver stack.
`solver.pop()`	Pops a context from the solver stack.
`solver.check()`	Checks the satisfiability of the current solver context.
`getMemObjAddress(var_id: int)`	Retrieves the memory object address for a given variable ID.
`loadValue(expr)`	Loads a value from a given Z3 expression.
`storeValue(lhs, rhs)`	Stores a value into a location.
`getGepOffset(stmt, ctx)`	Retrieves the offset for a GEP statement.
`getGepObjAddress(rhs, offset)`	Retrieves the address for a GEP object with a given offset.
`updateZ3Expr(idx: int, target)`	Updates the Z3 expression for a given index.
`getEvalExpr(e)`	Evaluates a Z3 expression and returns the result.

Method	Description
`createExprForObjVar(obj_var)`	Creates a Z3 expression for an object variable.
`getGepOffset(gep, callingCtx)`	Retrieves the offset for a GEP statement within a calling context.
`printExprValues(callingCtx)`	Prints the values of all Z3 expressions within a calling context.
`callingCtxToStr(callingCtx)`	Converts a calling context to a string representation.
`getZ3Expr(idx, callingCtx)`	Retrieves the Z3 expression for a given index and calling context.
`getEvalExpr(e)`	Evaluates a Z3 expression and returns the result.