55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
-
+
|
)
);
if( !result )
return true;
auto&& [type, val, locId] = *result;
auto paramVal = BuildComputedValue( type, llr::GetVar( type, varId++ ) );
auto paramVal = BuildComputedValue( type, llr::Load( llr::VarAddress( 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 );
|