klara.contract.solver.ContractSolver

class documentation

class ContractSolver(recipe.ClassInstanceBuilder): (source)

Undocumented

Method	`__init__`	Undocumented
Method	`post_conditions`	Undocumented
Method	`pre_conditions`	Undocumented
Method	`process_func_args`	from a function arguments, query the args from the z3 model, and use `model.eval(model_completion=True) for argument not part of constraint.
Method	`solve`	Undocumented
Method	`solve_function`	Undocumented
Method	`visit_functiondef`	Undocumented
Instance Variable	`as_tree`	Undocumented
Instance Variable	`cfg`	Undocumented
Instance Variable	`file_name`	Undocumented
Instance Variable	`functions`	Undocumented
Instance Variable	`id`	Undocumented
Method	`_gather_conditions`	Call `decorator` with `args`, gather Prm nodes and convert to z3 expr
Method	`_parse_args`	Return list of arg in function_args, order by decorator args. If decorator arg is in replace map, use the value of the map instead of the function :Raise: ValueError if arg in decorator doesn't exist in function...

Inherited from ClassInstanceBuilder:

Method	`visit_classdef`	Undocumented
Instance Variable	`class_ins`	Undocumented
Instance Variable	`context`	Undocumented

Inherited from AstVisitor (via ClassInstanceBuilder):

Method	`generic_visit`	Undocumented
Method	`visit`	Undocumented

def __init__(self, cfg, as_tree, file_name): (source)

overrides klara.core.recipe.ClassInstanceBuilder.__init__

Undocumented

def post_conditions(self, func, ret_val): (source)

Undocumented

Parameters
func	Undocumented
ret_val:`inference.InferenceResult`	Undocumented

def pre_conditions(self, func): (source)

Undocumented

Parameters
func:`nodes.FunctionDef`	Undocumented

def process_func_args(self, func, z3_result): (source)

from a function arguments, query the args from the z3 model, and use `model.eval(model_completion=True) for argument not part of constraint. For argument that contain defaults, if it's in the model, the arg will have the model's value. If it's not in the model, the defaults will be used.

Parameters
func:`nodes.FunctionDef`	Undocumented
z3_result	Undocumented
Returns
`List[ast_mod.Constant]`	Undocumented

def solve(self): (source)

Undocumented

Returns
`TestModule`	Undocumented

def solve_function(self, func): (source)

Undocumented

Parameters
func:`nodes.FunctionDef`	Undocumented
Returns
`TestCase`	Undocumented

def visit_functiondef(self, node): (source)

Undocumented

as_tree = (source)

Undocumented

cfg = (source)

Undocumented

file_name = (source)

Undocumented

functions: list = (source)

Undocumented

id: int = (source)

Undocumented

def _gather_conditions(self, args, decorator): (source)

Call `decorator` with `args`, gather Prm nodes and convert to z3 expr

Returns
`list`	Undocumented

def _parse_args(self, decorator_args, function_args, replace_map=None): (source)

Return list of arg in function_args, order by decorator args. If decorator arg is in replace map, use the value of the map instead of the function :Raise: ValueError if arg in decorator doesn't exist in function