27 if(expr.
id()==ID_symbol)
33 std::string identifier=
37 if(l0_l1!=std::string::npos)
39 identifier.resize(l0_l1);
57 if(assign.
rhs().
id()==ID_array)
74 else if(assign.
rhs().
id()==ID_struct ||
75 assign.
rhs().
id()==ID_union)
79 if(assign.
lhs().
id()==ID_member &&
87 else if(assign.
lhs().
id()==ID_byte_extract_little_endian ||
88 assign.
lhs().
id()==ID_byte_extract_big_endian)
101 exprt::operandst::const_iterator it=
103 for(
const auto &comp : components)
105 if(comp.type().id()==ID_code ||
106 comp.get_is_padding() ||
123 if(assign.
rhs().
id()==ID_union)
133 if(lhs.find(
'$')!=std::string::npos)
136 result=lhs+
" = "+
from_expr(
ns, identifier, clean_rhs)+
";";
144 const goto_tracet::stepst::const_iterator &prev_it,
145 goto_tracet::stepst::const_iterator &it)
148 (!it->pc->is_assign() ||
153 if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
159 if(prev_it!=goto_trace.
steps.end() &&
160 prev_it->pc->source_location==it->pc->source_location)
163 if(it->is_goto() && it->pc->guard.is_true())
168 if(source_location.
is_nil() ||
183 graphml[sink].node_name=
"sink";
185 graphml[sink].is_violation=
false;
186 graphml[sink].has_invariant=
false;
189 std::vector<std::size_t> step_to_node(goto_trace.
steps.size()+1, 0);
191 goto_tracet::stepst::const_iterator prev_it=goto_trace.
steps.end();
192 for(goto_tracet::stepst::const_iterator
193 it=goto_trace.
steps.begin();
194 it!=goto_trace.
steps.end();
199 step_to_node[it->step_nr]=sink;
205 goto_tracet::stepst::const_iterator next=it;
207 if(next!=goto_trace.
steps.end() &&
209 it->full_lhs==next->full_lhs &&
210 it->pc->source_location==next->pc->source_location)
212 step_to_node[it->step_nr]=sink;
226 graphml[node].thread_nr=it->thread_nr;
229 graphml[node].has_invariant=
false;
231 step_to_node[it->step_nr]=node;
235 for(goto_tracet::stepst::const_iterator
236 it=goto_trace.
steps.begin();
237 it!=goto_trace.
steps.end();
240 const std::size_t from=step_to_node[it->step_nr];
248 auto next = std::next(it);
249 for(; next != goto_trace.
steps.end() &&
250 (step_to_node[next->step_nr] == sink ||
256 const std::size_t to=
257 next==goto_trace.
steps.end()?
258 sink:step_to_node[next->step_nr];
281 it->lhs_object_value.is_not_nil() &&
282 it->full_lhs.is_not_nil())
284 if(!it->lhs_object_value.is_constant() ||
285 !it->lhs_object_value.has_operands() ||
291 code_assignt assign(it->lhs_object, it->lhs_object_value);
292 irep_idt identifier=it->lhs_object.get_identifier();
297 val_s.
data=
id2string(it->pc->source_location.get_function());
305 const std::string cond =
307 const std::string neg_cond=
309 val.
data=
"["+(it->cond_value ? cond : neg_cond)+
"]";
326 val2.
data=
"["+(it->cond_value ? neg_cond : cond)+
"]";
368 graphml[sink].node_name=
"sink";
370 graphml[sink].is_violation=
false;
371 graphml[sink].has_invariant=
false;
374 std::vector<std::size_t> step_to_node(equation.
SSA_steps.size()+1, 0);
376 std::size_t step_nr=1;
377 for(symex_target_equationt::SSA_stepst::const_iterator
385 (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
386 (it->is_goto() && it->source.pc->guard.is_true()) ||
387 source_location.
is_nil() ||
391 step_to_node[step_nr]=sink;
397 symex_target_equationt::SSA_stepst::const_iterator next=it;
400 next->is_assignment() &&
401 it->ssa_full_lhs==next->ssa_full_lhs &&
402 it->source.pc->source_location==next->source.pc->source_location)
404 step_to_node[step_nr]=sink;
415 graphml[node].thread_nr=it->source.thread_nr;
416 graphml[node].is_violation=
false;
417 graphml[node].has_invariant=
false;
419 step_to_node[step_nr]=node;
424 for(symex_target_equationt::SSA_stepst::const_iterator
429 const std::size_t from=step_to_node[step_nr];
438 symex_target_equationt::SSA_stepst::const_iterator next=it;
439 std::size_t next_step_nr=step_nr;
440 for(++next, ++next_step_nr;
442 (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
443 ++next, ++next_step_nr)
447 const std::size_t to=
449 sink:step_to_node[next_step_nr];
471 if((it->is_assignment() ||
473 it->ssa_rhs.is_not_nil() &&
474 it->ssa_full_lhs.is_not_nil())
476 irep_idt identifier=it->ssa_lhs.get_object_name();
478 graphml[to].has_invariant=
true;
482 id2string(it->source.pc->source_location.get_function());
484 else if(it->is_goto() &&
485 it->source.pc->is_goto())
489 const std::string cond =
490 from_expr(
ns, it->source.pc->function, it->cond_expr);
491 val.
data=
"["+cond+
"]";
520 step_nr=next_step_nr;
const std::string & id2string(const irep_idt &d)
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
static bool is_built_in(const std::string &s)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< componentt > componentst
const componentst & components() const
unsignedbv_typet size_type()
Extract member of struct or union.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Expression classes for byte-level operators.
const irep_idt & get_line() const
void remove_l0_l1(exprt &expr)
const edgest & out(node_indext n) const
void set_attribute(const std::string &attribute, unsigned value)
const irep_idt & get(const irep_namet &name) const
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
nodet::node_indext node_indext
const typet & follow(const typet &) const
bitvector_typet index_type()
Functor to check whether iterators from different collections point at the same object.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
xmlt & new_element(const std::string &name)
const irep_idt & get_file() const
Base type of C structs and unions, and C++ classes.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Base class for all expressions.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const exprt & get_original_expr() const
bool is_ssa_expr(const exprt &expr)
void set_identifier(const irep_idt &identifier)
const edgest & in(node_indext n) const
#define Forall_operands(it, expr)
void operator()(const goto_tracet &goto_trace)
counterexample witness
static bool filter_out(const goto_tracet &goto_trace, const goto_tracet::stepst::const_iterator &prev_it, goto_tracet::stepst::const_iterator &it)
const typet & subtype() const
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Witnesses for Traces and Proofs.