50 std::string identifier=
53 std::string::size_type
l0_l1=identifier.find_first_of(
"!@");
54 if(
l0_l1!=std::string::npos)
56 identifier.resize(
l0_l1);
79 if(cit !=
cache.end())
141 exprt::operandst::const_iterator it=
143 for(
const auto &
comp : components)
146 comp.type().id() !=
ID_code,
"struct member must not be of code type");
148 comp.get_is_padding() ||
150 comp.get_name().starts_with(
"$pad"))
154 it != assign.
rhs().
operands().end(),
"expression must have operands");
203 lhs.find(
"#return_value") != std::string::npos ||
204 (lhs.find(
'$') != std::string::npos &&
205 has_prefix(lhs,
"return_value___VERIFIER_nondet_")))
219 const goto_tracet::stepst::const_iterator &
prev_it,
220 goto_tracet::stepst::const_iterator &it)
224 (!it->pc->is_assign() || it->pc->assign_rhs().id() !=
ID_side_effect ||
228 if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
236 prev_it->pc->source_location() == it->pc->source_location())
239 if(it->is_goto() && it->pc->condition().is_true())
244 if(source_location.
is_nil() ||
245 source_location.
get_file().empty() ||
269 for(
const auto &op : expr.
operands())
282 for(goto_tracet::stepst::const_iterator it =
goto_trace.steps.begin();
288 if(it->is_assert() && !it->cond_value)
301 std::vector<graphmlt::node_indext> nodes;
306 graphml[nodes.back()].node_name =
"N" + std::to_string(i);
308 graphml[nodes.back()].has_invariant =
false;
311 for(
auto it = nodes.cbegin(); std::next(it) != nodes.cend(); ++it)
316 const auto thread_id = std::distance(nodes.cbegin(), it);
326 graphml[*std::next(it)].
in[*it].xml_node = edge;
327 graphml[*it].
out[*std::next(it)].xml_node = edge;
339 for(goto_tracet::stepst::const_iterator
352 goto_tracet::stepst::const_iterator next=it;
357 it->full_lhs == next->full_lhs &&
358 it->pc->source_location() == next->pc->source_location())
371 std::to_string(it->pc->location_number)+
"."+std::to_string(it->step_nr);
376 graphml[node].has_invariant=
false;
384 for(goto_tracet::stepst::const_iterator
398 auto next = std::next(it);
406 const std::size_t
to=
425 data_f.set_attribute(
"key",
"originfile");
429 data_l.set_attribute(
"key",
"startline");
433 data_t.set_attribute(
"key",
"threadId");
434 data_t.data = std::to_string(it->thread_nr);
443 if(
lhs_id.find(
"pthread_create::thread") != std::string::npos)
446 data_t.set_attribute(
"key",
"createThread");
454 lhs_id.find(
"thread") == std::string::npos &&
455 lhs_id.find(
"mutex") == std::string::npos &&
456 (!it->full_lhs_value.is_constant() ||
457 !it->full_lhs_value.has_operands() ||
463 xmlt &
val = edge.new_element(
"data");
464 val.set_attribute(
"key",
"assumption");
469 if(!it->function_id.empty())
472 val_s.set_attribute(
"key",
"assumption.scope");
473 irep_idt function_id = it->function_id;
485 val_f.set_attribute(
"key",
"assumption.resultfunction");
536 std::size_t step_nr=1;
537 for(symex_target_equationt::SSA_stepst::const_iterator
546 (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
547 (it->is_goto() && it->source.pc->condition().is_true()) ||
557 symex_target_equationt::SSA_stepst::const_iterator next=it;
560 next != equation.
SSA_steps.end() && next->is_assignment() &&
561 it->ssa_full_lhs == next->ssa_full_lhs &&
562 it->source.pc->source_location() == next->source.pc->source_location())
571 std::to_string(it->source.pc->location_number)+
"."+
572 std::to_string(step_nr);
575 graphml[node].is_violation=
false;
576 graphml[node].has_invariant=
false;
583 for(symex_target_equationt::SSA_stepst::const_iterator
597 symex_target_equationt::SSA_stepst::const_iterator next=it;
606 const std::size_t
to=
625 data_f.set_attribute(
"key",
"originfile");
629 data_l.set_attribute(
"key",
"startline");
634 (it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
635 it->ssa_full_lhs.is_not_nil())
637 irep_idt identifier = it->ssa_lhs.get_object_name();
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet c_index_type()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from a list of index-element pairs Operands are index/value pairs,...
const typet & element_type() const
The type of the elements of the array.
A goto_instruction_codet representing an assignment in the program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
void operator()(const goto_tracet &goto_trace)
counterexample witness
std::unordered_map< std::pair< unsigned int, const irept::dt * >, std::string, pair_hash< unsigned int, const irept::dt * > > cache
void remove_l0_l1(exprt &expr)
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
nodet::node_indext node_indext
const edgest & out(node_indext n) const
node_indext add_node(arguments &&... values)
const edgest & in(node_indext n) const
const irep_idt & id() const
Extract member of struct or union.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const irep_idt & get_function() const
const irep_idt & get_file() const
const irep_idt & get_line() const
static bool is_built_in(const std::string &s)
std::vector< componentt > componentst
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
The type of an expression, extends irept.
Operator to update elements in structs and arrays.
xmlt & new_element(const std::string &key)
void set_attribute(const std::string &attribute, unsigned value)
static bool is_printable_xml(const std::string &s)
Determine whether s does not contain any characters that cannot be escaped in XML 1....
bool has_prefix(const std::string &s, const std::string &prefix)
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
#define Forall_operands(it, expr)
static std::string expr_to_string(const namespacet &ns, const irep_idt &id, const exprt &expr)
static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
static bool filter_out(const goto_tracet &goto_trace, const goto_tracet::stepst::const_iterator &prev_it, goto_tracet::stepst::const_iterator &it)
Witnesses for Traces and Proofs.
const std::string & id2string(const irep_idt &d)
const std::string thread_id
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const irep_idt & get_mode_from_identifier(const namespacet &ns, const irep_idt &identifier)
Get the mode of the given identifier's symbol.
Various predicates over pointers in programs.
#define SYMEX_DYNAMIC_PREFIX
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
bool is_ssa_expr(const exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const array_list_exprt & to_array_list_expr(const exprt &expr)
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const string_constantt & to_string_constant(const exprt &expr)
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
Functor to check whether iterators from different collections point at the same object.
Generate Equation using Symbolic Execution.