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;
114 symex_target_equationt::SSA_stepst::const_iterator end_step,
123 typedef std::map<mp_integer, goto_tracet::stepst> time_mapt;
129 bool end_step_seen=
false;
131 for(symex_target_equationt::SSA_stepst::const_iterator
144 if(it->is_constraint() ||
147 else if(it->is_atomic_begin())
156 else if(it->is_shared_read() || it->is_shared_write() ||
161 if(it->is_shared_read() || it->is_shared_write())
169 else if(it->is_atomic_end() && current_time<0)
172 assert(current_time>=0);
177 time_mapt::iterator entry=
178 time_map.insert(std::make_pair(
181 entry->second.splice(entry->second.end(), time_map[time_before]);
182 time_map.erase(time_before);
189 if(it->is_assignment() &&
202 end_ptr=&goto_trace_step;
205 goto_trace_step.
pc=SSA_step.
source.pc;
220 (it->is_assignment()&&
244 if(j.is_constant() ||
245 j.id()==ID_string_constant)
246 goto_trace_step.
io_args.push_back(j);
250 goto_trace_step.
io_args.push_back(tmp);
267 for(
auto &t_it : time_map)
268 goto_trace.
steps.splice(goto_trace.
steps.end(), t_it.second);
271 for(goto_tracet::stepst::iterator
272 s_it1=goto_trace.
steps.begin();
273 s_it1!=goto_trace.
steps.end();
275 if(end_step_seen && end_ptr==&(*s_it1))
284 for(
auto &s_it : goto_trace.
steps)
285 s_it.step_nr=++step_nr;
295 target, target.
SSA_steps.end(), prop_conv, ns, goto_trace);
298 for(goto_tracet::stepst::iterator
299 s_it1=goto_trace.
steps.begin();
300 s_it1!=goto_trace.
steps.end();
302 if(s_it1->is_assert() && !s_it1->cond_value)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
void trim_after(stepst::iterator s)
std::list< goto_trace_stept > stepst
virtual exprt get(const exprt &expr) const =0
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
The trinary if-then-else operator.
assignment_typet assignment_type
std::list< exprt > converted_io_args
goto_programt::const_targett pc
Add constraints to equation encoding partial orders on events.
Extract member of struct or union.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
static irep_idt rw_clock_id(event_it e, axiomt axiom=AX_PROPAGATION)
const irep_idt & id() const
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
exprt adjust_lhs_object(const prop_convt &prop_conv, const namespacet &ns, const exprt &src)
virtual tvt l_get(literalt a) const =0
absolute_timet current_time()
exprt build_full_lhs_rec(const prop_convt &prop_conv, const namespacet &ns, const exprt &src_original, const exprt &src_ssa)
Base class for all expressions.
const exprt & struct_op() const
const exprt & get_original_expr() const
Expression to hold a symbol (variable)
goto_trace_stept::typet type
Expression providing an SSA-renamed symbol of expressions.
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)
bool simplify(exprt &expr, const namespacet &ns)
assignment_typet assignment_type