30 const exprt &src_original,
33 if(src_ssa.
id()!=src_original.
id())
47 tmp.
index()=index_value;
57 else if(
id==ID_member)
79 else if(tmp.is_false())
84 else if(
id==ID_typecast)
91 else if(
id==ID_byte_extract_little_endian ||
92 id==ID_byte_extract_big_endian)
94 exprt tmp=src_original;
119 if(expr.
id()==ID_symbol)
123 if(!ns.
lookup(
id, symbol))
151 if(SSA_step.
source.pc->source_location.as_string().empty())
168 if(SSA_step.
source.pc->code.get_statement()!=ID_function_call)
175 symex_target_equationt::SSA_stepst::const_iterator end_step,
184 typedef std::map<mp_integer, goto_tracet::stepst> time_mapt;
190 bool end_step_seen=
false;
192 for(symex_target_equationt::SSA_stepst::const_iterator
205 if(it->is_constraint() ||
208 else if(it->is_atomic_begin())
217 else if(it->is_shared_read() || it->is_shared_write() ||
222 if(it->is_shared_read() || it->is_shared_write())
230 else if(it->is_atomic_end() && current_time<0)
233 assert(current_time>=0);
238 time_mapt::iterator entry=
239 time_map.insert(std::make_pair(
242 entry->second.splice(entry->second.end(), time_map[time_before]);
243 time_map.erase(time_before);
250 if(it->is_assignment() &&
263 end_ptr=&goto_trace_step;
266 goto_trace_step.
pc=SSA_step.
source.pc;
284 (it->is_assignment()&&
308 if(j.is_constant() ||
309 j.id()==ID_string_constant)
310 goto_trace_step.
io_args.push_back(j);
314 goto_trace_step.
io_args.push_back(tmp);
331 for(
auto &t_it : time_map)
332 goto_trace.
steps.splice(goto_trace.
steps.end(), t_it.second);
335 for(goto_tracet::stepst::iterator
336 s_it1=goto_trace.
steps.begin();
337 s_it1!=goto_trace.
steps.end();
339 if(end_step_seen && end_ptr==&(*s_it1))
348 for(
auto &s_it : goto_trace.
steps)
349 s_it.step_nr=++step_nr;
359 target, target.
SSA_steps.end(), prop_conv, ns, goto_trace);
362 for(goto_tracet::stepst::iterator
363 s_it1=goto_trace.
steps.begin();
364 s_it1!=goto_trace.
steps.end();
366 if(s_it1->is_assert() && !s_it1->cond_value)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
void trim_after(stepst::iterator s)
exprt adjust_lhs_object(const prop_convt &prop_conv, const namespacet &ns, const exprt &src)
std::list< goto_trace_stept > stepst
virtual exprt get(const exprt &expr) const =0
bool is_function_call() const
The trinary if-then-else operator.
assignment_typet assignment_type
std::list< exprt > converted_io_args
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
bool get_bool(const irep_namet &name) const
goto_programt::const_targett pc
Add constraints to equation encoding partial orders on events.
Extract member of struct or union.
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const irep_idt get_original_name() const
#define forall_operands(it, expr)
void build_goto_trace(const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator end_step, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
typet type
Type of symbol.
virtual tvt l_get(literalt a) const =0
static irep_idt entry_point()
Base class for all expressions.
const exprt & struct_op() const
const exprt & get_original_expr() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
void update_internal_field(const symex_target_equationt::SSA_stept &SSA_step, goto_trace_stept &goto_trace_step, const namespacet &ns)
set internal for variables assignments related to dynamic_object and CPROVER internal functions (e...
exprt build_full_lhs_rec(const prop_convt &prop_conv, const namespacet &ns, const exprt &src_original, const exprt &src_ssa)
Expression to hold a symbol (variable)
goto_trace_stept::typet type
Expression providing an SSA-renamed symbol of expressions.
void set_internal_dynamic_object(const exprt &expr, goto_trace_stept &goto_trace_step, const namespacet &ns)
set internal field for variable assignment related to dynamic_object[0-9] and dynamic_[0-9]_array.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
bool simplify(exprt &expr, const namespacet &ns)
assignment_typet assignment_type