155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
|
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
|
-
-
+
+
+
+
+
+
+
+
+
+
+
+
|
optional< Z3Val > BuildZ3Op( Builder& b, const Load& instr )
{
return LoadFromAddress( b, *instr.addr() );
}
optional< Z3Val > BuildZ3Op( Builder& b, const Store& instr )
{
if( auto zv = BuildZ3ExprFromValue( b, instr.val() ) )
StoreToAddress( b, *instr.addr(), move( *zv ) );
auto zv = BuildZ3ExprFromValue( b, instr.val() );
if( !zv )
return nullopt;
ForEachPredicate( b, instr.type(), zv->expr, [&]( auto&& z3expr, auto locId )
{
DiagnosticsContext dc( instr.destLocId(), "...to this." );
DiagnosticsContext dc2( instr.val().locationId(), "When assigning this..." );
b.checkAssertion( z3expr, locId );
} );
StoreToAddress( b, *instr.addr(), move( *zv ) );
return nullopt;
}
// Implemented in call.cpp
extern optional< Z3Val > BuildZ3Op( Builder& b, const Call& instr );
optional< Z3Val > BuildZ3Op( Builder& b, const CreateTemporary& instr )
|