28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
// 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 )
{
auto arg = *ValueFromEIR( t );
if( auto zv = BuildZ3ExprFromValue( b, arg ) )
cb.setVar( index++, move( *zv ) );
return true;
} );
|
|
|
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
// 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 )
{
auto arg = *EIRToValue( t );
if( auto zv = BuildZ3ExprFromValue( b, arg ) )
cb.setVar( index++, move( *zv ) );
return true;
} );
|
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
if( retExpr )
cb.setPlaceholder( "@result"_sid, retExpr->expr );
// Check preconditions.
const auto& preConds = fvi->preConditions();
ForEachInVectorTerm( preConds, [&]( auto&& t )
{
auto val = *ValueFromEIR( t );
if( auto zv = BuildZ3ExprFromValue( cb, val ) )
{
DiagnosticsContext dc( instr.func().locationId(), "At this call." );
b.checkAssertion( zv->expr, val.locationId() );
}
return true;
} );
// Add the return type's predicates as assumptions.
ForEachPredicate( cb, ft.returnType(), retExpr->expr, [&]( auto&& z3expr, auto locId )
{
b.assume( z3expr );
} );
// Add postconditions as assumptions.
const auto& postConds = fvi->postConditions();
ForEachInVectorTerm( postConds, [&]( auto&& t )
{
if( auto zv = BuildZ3ExprFromValue( cb, *ValueFromEIR( t ) ) )
b.assume( zv->expr );
return true;
} );
return retExpr;
}
}
|
|
|
|
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
if( retExpr )
cb.setPlaceholder( "@result"_sid, retExpr->expr );
// Check preconditions.
const auto& preConds = fvi->preConditions();
ForEachInVectorTerm( preConds, [&]( auto&& t )
{
auto val = *EIRToValue( t );
if( auto zv = BuildZ3ExprFromValue( cb, val ) )
{
DiagnosticsContext dc( instr.func().locationId(), "At this call." );
b.checkAssertion( zv->expr, val.locationId() );
}
return true;
} );
// Add the return type's predicates as assumptions.
ForEachPredicate( cb, ft.returnType(), retExpr->expr, [&]( auto&& z3expr, auto locId )
{
b.assume( z3expr );
} );
// Add postconditions as assumptions.
const auto& postConds = fvi->postConditions();
ForEachInVectorTerm( postConds, [&]( auto&& t )
{
if( auto zv = BuildZ3ExprFromValue( cb, *EIRToValue( t ) ) )
b.assume( zv->expr );
return true;
} );
return retExpr;
}
}
|