SVF Python Z3 API

Z3Mgr API Documentation

Z3Mgr

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.

SSE

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.