150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
|
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
|
-
+
-
+
|
optional< Z3Val > BuildZ3Op( Builder& b, const T& instr )
{
return nullopt;
}
optional< Z3Val > BuildZ3Op( Builder& b, const Load& instr )
{
return LoadFromAddress( b, instr.addr() );
return LoadFromAddress( b, FromValue< builtins::Reference >( instr.addr() )->address() );
}
optional< Z3Val > BuildZ3Op( Builder& b, const Store& instr )
{
if( auto zv = BuildZ3ExprFromValue( b, instr.val() ) )
StoreToAddress( b, instr.addr(), move( *zv ) );
StoreToAddress( b, FromValue< builtins::Reference >( instr.addr() )->address(), 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 )
|