19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
auto retExpr = BuildZ3ConstantFromType( b, ft.returnType(), format( "r{}", b.newUniqueId() ) );
// Create a temporary builder to construct the z3 expressions out of the
// function's pre-conditions and postconditions, configured
// to perform the necessary replacements for arguments and for the
// return value placeholder.
Builder cb( b.context(), *b.solver(), b.remapper() );
cb.setAssertionHandler( b.GetAssertionHandler() );
// Inject the arguments in the context.
// They will be picked up by getVars instructions when refered to
// by the verification conditions.
uint32_t index = 0;
ForEachInVectorTerm( instr.args(), [&]( auto&& t )
|
|
|
|
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
auto retExpr = BuildZ3ConstantFromType( b, ft.returnType(), format( "r{}", b.newUniqueId() ) );
// Create a temporary builder to construct the z3 expressions out of the
// function's pre-conditions and postconditions, configured
// to perform the necessary replacements for arguments and for the
// return value placeholder.
Builder cb( b.context(), *b.solver(), b.getPredsDict(), b.remapper() );
cb.setAssertionHandler( b.getAssertionHandler() );
// Inject the arguments in the context.
// They will be picked up by getVars instructions when refered to
// by the verification conditions.
uint32_t index = 0;
ForEachInVectorTerm( instr.args(), [&]( auto&& t )
|