150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
|
optional< Z3Val > BuildZ3Op( Builder& b, const T& instr )
{
return nullopt;
}
optional< Z3Val > BuildZ3Op( Builder& b, const Load& instr )
{
return LoadFromAddress( b, *instr.addr() );
}
optional< Z3Val > BuildZ3Op( Builder& b, const Store& instr )
{
auto zv = BuildZ3ExprFromValue( b, instr.val() );
if( !zv )
return nullopt;
|
|
>
>
>
>
>
>
>
>
>
|
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
optional< Z3Val > BuildZ3Op( Builder& b, const T& instr )
{
return nullopt;
}
optional< Z3Val > BuildZ3Op( Builder& b, const Load& instr )
{
auto zv = LoadFromAddress( b, *instr.addr() );
if( !zv )
return nullopt;
ForEachPredicate( b, instr.type(), zv->expr, [&]( auto&& z3expr, auto locId )
{
b.assume( z3expr );
} );
return zv;
}
optional< Z3Val > BuildZ3Op( Builder& b, const Store& instr )
{
auto zv = BuildZ3ExprFromValue( b, instr.val() );
if( !zv )
return nullopt;
|