20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
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 )
|
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
-
+
-
-
-
-
-
-
-
+
+
+
+
-
|
)
);
if( !result )
return true;
auto&& [type, val, locId] = *result;
auto paramVal = BuildComputedValue( type, VarAddr( varId++ ) );
auto paramVal = BuildComputedValue( type, Load( make_shared< Instruction >( VarAddr( varId++ ) ), type ) );
if( auto zv = BuildZ3ExprFromValue( cb, paramVal ) )
{
ForEachPredicate( cb, type, zv->expr, [&]( auto&& z3expr, auto locId )
{
DiagnosticsContext dc( instr.func().locationId(), "At this call." );
b.checkAssertion( z3expr, locId );
} );
}
|