69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
)
);
if( !result )
return true;
auto&& [type, val, locId] = *result;
auto paramVal = BuildComputedValue( type, VarAddr( varId++, type, locId ), Load( type, locId ) );
auto zv = BuildZ3ExprFromValue( cb, paramVal );
ForEachPredicate( cb, type, zv.expr, [&]( auto&& z3expr, auto locId )
{
DiagnosticsContext dc( fVal->locationId(), "At this call." );
b.checkAssertion( z3expr, locId );
} );
|
|
|
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
)
);
if( !result )
return true;
auto&& [type, val, locId] = *result;
auto paramVal = BuildComputedValue( type, VarAddr( varId++, locId ), Load( type, locId ) );
auto zv = BuildZ3ExprFromValue( cb, paramVal );
ForEachPredicate( cb, type, zv.expr, [&]( auto&& z3expr, auto locId )
{
DiagnosticsContext dc( fVal->locationId(), "At this call." );
b.checkAssertion( z3expr, locId );
} );
|