cprover
graphml_witness.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Witnesses for Traces and Proofs
4 
5 Author: Daniel Kroening
6 
7 \*******************************************************************/
8 
11 
12 #include "graphml_witness.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/byte_operators.h>
16 #include <util/c_types.h>
17 #include <util/cprover_prefix.h>
19 #include <util/prefix.h>
20 #include <util/ssa_expr.h>
21 #include <util/string_container.h>
22 
23 #include <langapi/language_util.h>
24 #include <langapi/mode.h>
25 
26 #include <ansi-c/expr2c.h>
27 
28 #include "goto_program.h"
29 
30 static std::string
31 expr_to_string(const namespacet &ns, const irep_idt &id, const exprt &expr)
32 {
33  if(get_mode_from_identifier(ns, id) == ID_C)
35  else
36  return from_expr(ns, id, expr);
37 }
38 
40 {
41  if(expr.id()==ID_symbol)
42  {
43  if(is_ssa_expr(expr))
44  expr=to_ssa_expr(expr).get_original_expr();
45  else
46  {
47  std::string identifier=
48  id2string(to_symbol_expr(expr).get_identifier());
49 
50  std::string::size_type l0_l1=identifier.find_first_of("!@");
51  if(l0_l1!=std::string::npos)
52  {
53  identifier.resize(l0_l1);
54  to_symbol_expr(expr).set_identifier(identifier);
55  }
56  }
57 
58  return;
59  }
60 
61  Forall_operands(it, expr)
62  remove_l0_l1(*it);
63 }
64 
66  const irep_idt &identifier,
67  const code_assignt &assign)
68 {
69 #ifdef USE_DSTRING
70  const auto cit = cache.find({identifier.get_no(), &assign.read()});
71 #else
72  const auto cit =
73  cache.find({get_string_container()[id2string(identifier)], &assign.read()});
74 #endif
75  if(cit != cache.end())
76  return cit->second;
77 
78  std::string result;
79 
80  if(assign.rhs().id() == ID_array_list)
81  {
82  const array_list_exprt &array_list = to_array_list_expr(assign.rhs());
83  const auto &ops = array_list.operands();
84 
85  for(std::size_t listidx = 0; listidx != ops.size(); listidx += 2)
86  {
87  const index_exprt index{assign.lhs(), ops[listidx]};
88  if(!result.empty())
89  result += ' ';
90  result +=
91  convert_assign_rec(identifier, code_assignt{index, ops[listidx + 1]});
92  }
93  }
94  else if(assign.rhs().id() == ID_array)
95  {
96  const array_typet &type = to_array_type(assign.rhs().type());
97 
98  unsigned i=0;
99  forall_operands(it, assign.rhs())
100  {
101  index_exprt index(
102  assign.lhs(),
103  from_integer(i++, index_type()),
104  type.subtype());
105  if(!result.empty())
106  result+=' ';
107  result+=convert_assign_rec(identifier, code_assignt(index, *it));
108  }
109  }
110  else if(assign.rhs().id()==ID_struct ||
111  assign.rhs().id()==ID_union)
112  {
113  // dereferencing may have resulted in an lhs that is the first
114  // struct member; undo this
115  if(
116  assign.lhs().id() == ID_member &&
117  assign.lhs().type() != assign.rhs().type())
118  {
119  code_assignt tmp=assign;
120  tmp.lhs()=to_member_expr(assign.lhs()).struct_op();
121 
122  return convert_assign_rec(identifier, tmp);
123  }
124  else if(assign.lhs().id()==ID_byte_extract_little_endian ||
125  assign.lhs().id()==ID_byte_extract_big_endian)
126  {
127  code_assignt tmp=assign;
128  tmp.lhs()=to_byte_extract_expr(assign.lhs()).op();
129 
130  return convert_assign_rec(identifier, tmp);
131  }
132 
133  const struct_union_typet &type=
134  to_struct_union_type(ns.follow(assign.lhs().type()));
135  const struct_union_typet::componentst &components=
136  type.components();
137 
138  exprt::operandst::const_iterator it=
139  assign.rhs().operands().begin();
140  for(const auto &comp : components)
141  {
142  if(comp.type().id()==ID_code ||
143  comp.get_is_padding() ||
144  // for some reason #is_padding gets lost in *some* cases
145  has_prefix(id2string(comp.get_name()), "$pad"))
146  continue;
147 
148  INVARIANT(
149  it != assign.rhs().operands().end(), "expression must have operands");
150 
151  member_exprt member(
152  assign.lhs(),
153  comp.get_name(),
154  it->type());
155  if(!result.empty())
156  result+=' ';
157  result+=convert_assign_rec(identifier, code_assignt(member, *it));
158  ++it;
159 
160  // for unions just assign to the first member
161  if(assign.rhs().id()==ID_union)
162  break;
163  }
164  }
165  else if(assign.rhs().id() == ID_with)
166  {
167  const with_exprt &with_expr = to_with_expr(assign.rhs());
168  const auto &ops = with_expr.operands();
169 
170  for(std::size_t i = 1; i < ops.size(); i += 2)
171  {
172  if(!result.empty())
173  result += ' ';
174 
175  if(ops[i].id() == ID_member_name)
176  {
177  const member_exprt member{
178  assign.lhs(), ops[i].get(ID_component_name), ops[i + 1].type()};
179  result +=
180  convert_assign_rec(identifier, code_assignt(member, ops[i + 1]));
181  }
182  else
183  {
184  const index_exprt index{assign.lhs(), ops[i]};
185  result +=
186  convert_assign_rec(identifier, code_assignt(index, ops[i + 1]));
187  }
188  }
189  }
190  else
191  {
192  exprt clean_rhs=assign.rhs();
193  remove_l0_l1(clean_rhs);
194 
195  exprt clean_lhs = assign.lhs();
196  remove_l0_l1(clean_lhs);
197  std::string lhs = expr_to_string(ns, identifier, clean_lhs);
198 
199  if(
200  lhs.find("#return_value") != std::string::npos ||
201  (lhs.find('$') != std::string::npos &&
202  has_prefix(lhs, "return_value___VERIFIER_nondet_")))
203  {
204  lhs="\\result";
205  }
206 
207  result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";";
208  }
209 
210 #ifdef USE_DSTRING
211  cache.insert({{identifier.get_no(), &assign.read()}, result});
212 #else
213  cache.insert(
214  {{get_string_container()[id2string(identifier)], &assign.read()}, result});
215 #endif
216  return result;
217 }
218 
219 static bool filter_out(
220  const goto_tracet &goto_trace,
221  const goto_tracet::stepst::const_iterator &prev_it,
222  goto_tracet::stepst::const_iterator &it)
223 {
224  if(
225  it->hidden && (!it->pc->is_assign() ||
226  it->pc->get_assign().rhs().id() != ID_side_effect ||
227  it->pc->get_assign().rhs().get(ID_statement) != ID_nondet))
228  return true;
229 
230  if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
231  return true;
232 
233  // we filter out steps with the same source location
234  // TODO: if these are assignments we should accumulate them into
235  // a single edge
236  if(prev_it!=goto_trace.steps.end() &&
237  prev_it->pc->source_location==it->pc->source_location)
238  return true;
239 
240  if(it->is_goto() && it->pc->get_condition().is_true())
241  return true;
242 
243  const source_locationt &source_location=it->pc->source_location;
244 
245  if(source_location.is_nil() ||
246  source_location.get_file().empty() ||
247  source_location.is_built_in() ||
248  source_location.get_line().empty())
249  {
250  const irep_idt id = source_location.get_function();
251  // Do not filter out assertions in functions the name of which starts with
252  // CPROVER_PREFIX, because we need to maintain those as violation nodes:
253  // these are assertions generated, for examples, for memory leaks.
254  if(!has_prefix(id2string(id), CPROVER_PREFIX) || !it->is_assert())
255  return true;
256  }
257 
258  return false;
259 }
260 
261 static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
262 {
263  if(
264  expr.id() == ID_symbol &&
265  has_prefix(id2string(to_symbol_expr(expr).get_identifier()), prefix))
266  {
267  return true;
268  }
269 
270  forall_operands(it, expr)
271  {
272  if(contains_symbol_prefix(*it, prefix))
273  return true;
274  }
275  return false;
276 }
277 
280 {
281  unsigned int max_thread_idx = 0;
282  bool trace_has_violation = false;
283  for(goto_tracet::stepst::const_iterator it = goto_trace.steps.begin();
284  it != goto_trace.steps.end();
285  ++it)
286  {
287  if(it->thread_nr > max_thread_idx)
288  max_thread_idx = it->thread_nr;
289  if(it->is_assert() && !it->cond_value)
290  trace_has_violation = true;
291  }
292 
293  graphml.key_values["sourcecodelang"]="C";
294 
296  graphml[sink].node_name="sink";
297  graphml[sink].is_violation=false;
298  graphml[sink].has_invariant=false;
299 
300  if(max_thread_idx > 0 && trace_has_violation)
301  {
302  std::vector<graphmlt::node_indext> nodes;
303 
304  for(unsigned int i = 0; i <= max_thread_idx + 1; ++i)
305  {
306  nodes.push_back(graphml.add_node());
307  graphml[nodes.back()].node_name = "N" + std::to_string(i);
308  graphml[nodes.back()].is_violation = i == max_thread_idx + 1;
309  graphml[nodes.back()].has_invariant = false;
310  }
311 
312  for(auto it = nodes.cbegin(); std::next(it) != nodes.cend(); ++it)
313  {
314  xmlt edge("edge");
315  edge.set_attribute("source", graphml[*it].node_name);
316  edge.set_attribute("target", graphml[*std::next(it)].node_name);
317  const auto thread_id = std::distance(nodes.cbegin(), it);
318  xmlt &data = edge.new_element("data");
319  data.set_attribute("key", "createThread");
320  data.data = std::to_string(thread_id);
321  if(thread_id == 0)
322  {
323  xmlt &data = edge.new_element("data");
324  data.set_attribute("key", "enterFunction");
325  data.data = "main";
326  }
327  graphml[*std::next(it)].in[*it].xml_node = edge;
328  graphml[*it].out[*std::next(it)].xml_node = edge;
329  }
330 
331  // we do not provide any further details as CPAchecker does not seem to
332  // handle more detailed concurrency witnesses
333  return;
334  }
335 
336  // step numbers start at 1
337  std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
338 
339  goto_tracet::stepst::const_iterator prev_it=goto_trace.steps.end();
340  for(goto_tracet::stepst::const_iterator
341  it=goto_trace.steps.begin();
342  it!=goto_trace.steps.end();
343  it++) // we cannot replace this by a ranged for
344  {
345  if(filter_out(goto_trace, prev_it, it))
346  {
347  step_to_node[it->step_nr]=sink;
348 
349  continue;
350  }
351 
352  // skip declarations followed by an immediate assignment
353  goto_tracet::stepst::const_iterator next=it;
354  ++next;
355  if(next!=goto_trace.steps.end() &&
357  it->full_lhs==next->full_lhs &&
358  it->pc->source_location==next->pc->source_location)
359  {
360  step_to_node[it->step_nr]=sink;
361 
362  continue;
363  }
364 
365  prev_it=it;
366 
367  const source_locationt &source_location=it->pc->source_location;
368 
370  graphml[node].node_name=
371  std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr);
372  graphml[node].file=source_location.get_file();
373  graphml[node].line=source_location.get_line();
374  graphml[node].is_violation=
375  it->type==goto_trace_stept::typet::ASSERT && !it->cond_value;
376  graphml[node].has_invariant=false;
377 
378  step_to_node[it->step_nr]=node;
379  }
380 
381  unsigned thread_id = 0;
382 
383  // build edges
384  for(goto_tracet::stepst::const_iterator
385  it=goto_trace.steps.begin();
386  it!=goto_trace.steps.end();
387  ) // no ++it
388  {
389  const std::size_t from=step_to_node[it->step_nr];
390 
391  // no outgoing edges from sinks or violation nodes
392  if(from == sink || graphml[from].is_violation)
393  {
394  ++it;
395  continue;
396  }
397 
398  auto next = std::next(it);
399  for(; next != goto_trace.steps.end() &&
400  (step_to_node[next->step_nr] == sink ||
401  pointee_address_equalt{}(it->pc, next->pc)); // NOLINT
402  ++next)
403  {
404  // advance
405  }
406  const std::size_t to=
407  next==goto_trace.steps.end()?
408  sink:step_to_node[next->step_nr];
409 
410  switch(it->type)
411  {
416  {
417  xmlt edge(
418  "edge",
419  {{"source", graphml[from].node_name},
420  {"target", graphml[to].node_name}},
421  {});
422 
423  {
424  xmlt &data_f = edge.new_element("data");
425  data_f.set_attribute("key", "originfile");
426  data_f.data = id2string(graphml[from].file);
427 
428  xmlt &data_l = edge.new_element("data");
429  data_l.set_attribute("key", "startline");
430  data_l.data = id2string(graphml[from].line);
431 
432  xmlt &data_t = edge.new_element("data");
433  data_t.set_attribute("key", "threadId");
434  data_t.data = std::to_string(it->thread_nr);
435  }
436 
437  const auto lhs_object = it->get_lhs_object();
438  if(
440  lhs_object.has_value())
441  {
442  const std::string &lhs_id = id2string(lhs_object->get_identifier());
443  if(lhs_id.find("pthread_create::thread") != std::string::npos)
444  {
445  xmlt &data_t = edge.new_element("data");
446  data_t.set_attribute("key", "createThread");
447  data_t.data = std::to_string(++thread_id);
448  }
449  else if(
451  it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
453  it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
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() ||
458  !has_prefix(
459  id2string(
460  to_multi_ary_expr(it->full_lhs_value).op0().get(ID_value)),
461  "INVALID-")))
462  {
463  xmlt &val = edge.new_element("data");
464  val.set_attribute("key", "assumption");
465 
466  code_assignt assign{it->full_lhs, it->full_lhs_value};
467  val.data = convert_assign_rec(lhs_id, assign);
468 
469  xmlt &val_s = edge.new_element("data");
470  val_s.set_attribute("key", "assumption.scope");
471  irep_idt function_id = it->function_id;
472  const symbolt *symbol_ptr = nullptr;
473  if(!ns.lookup(lhs_id, symbol_ptr) && symbol_ptr->is_parameter)
474  {
475  function_id = lhs_id.substr(0, lhs_id.find("::"));
476  }
477  val_s.data = id2string(function_id);
478 
479  if(has_prefix(val.data, "\\result ="))
480  {
481  xmlt &val_f = edge.new_element("data");
482  val_f.set_attribute("key", "assumption.resultfunction");
483  val_f.data = id2string(it->function_id);
484  }
485  }
486  }
487  else if(it->type == goto_trace_stept::typet::GOTO && it->pc->is_goto())
488  {
489  }
490 
491  graphml[to].in[from].xml_node = edge;
492  graphml[from].out[to].xml_node = edge;
493 
494  break;
495  }
496 
512  // ignore
513  break;
514  }
515 
516  it=next;
517  }
518 }
519 
522 {
523  graphml.key_values["sourcecodelang"]="C";
524 
526  graphml[sink].node_name="sink";
527  graphml[sink].is_violation=false;
528  graphml[sink].has_invariant=false;
529 
530  // step numbers start at 1
531  std::vector<std::size_t> step_to_node(equation.SSA_steps.size()+1, 0);
532 
533  std::size_t step_nr=1;
534  for(symex_target_equationt::SSA_stepst::const_iterator
535  it=equation.SSA_steps.begin();
536  it!=equation.SSA_steps.end();
537  it++, step_nr++) // we cannot replace this by a ranged for
538  {
539  const source_locationt &source_location=it->source.pc->source_location;
540 
541  if(
542  it->hidden ||
543  (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
544  (it->is_goto() && it->source.pc->get_condition().is_true()) ||
545  source_location.is_nil() || source_location.is_built_in() ||
546  source_location.get_line().empty())
547  {
548  step_to_node[step_nr]=sink;
549 
550  continue;
551  }
552 
553  // skip declarations followed by an immediate assignment
554  symex_target_equationt::SSA_stepst::const_iterator next=it;
555  ++next;
556  if(next!=equation.SSA_steps.end() &&
557  next->is_assignment() &&
558  it->ssa_full_lhs==next->ssa_full_lhs &&
559  it->source.pc->source_location==next->source.pc->source_location)
560  {
561  step_to_node[step_nr]=sink;
562 
563  continue;
564  }
565 
567  graphml[node].node_name=
568  std::to_string(it->source.pc->location_number)+"."+
569  std::to_string(step_nr);
570  graphml[node].file=source_location.get_file();
571  graphml[node].line=source_location.get_line();
572  graphml[node].is_violation=false;
573  graphml[node].has_invariant=false;
574 
575  step_to_node[step_nr]=node;
576  }
577 
578  // build edges
579  step_nr=1;
580  for(symex_target_equationt::SSA_stepst::const_iterator
581  it=equation.SSA_steps.begin();
582  it!=equation.SSA_steps.end();
583  ) // no ++it
584  {
585  const std::size_t from=step_to_node[step_nr];
586 
587  if(from==sink)
588  {
589  ++it;
590  ++step_nr;
591  continue;
592  }
593 
594  symex_target_equationt::SSA_stepst::const_iterator next=it;
595  std::size_t next_step_nr=step_nr;
596  for(++next, ++next_step_nr;
597  next!=equation.SSA_steps.end() &&
598  (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
599  ++next, ++next_step_nr)
600  {
601  // advance
602  }
603  const std::size_t to=
604  next==equation.SSA_steps.end()?
605  sink:step_to_node[next_step_nr];
606 
607  switch(it->type)
608  {
613  {
614  xmlt edge(
615  "edge",
616  {{"source", graphml[from].node_name},
617  {"target", graphml[to].node_name}},
618  {});
619 
620  {
621  xmlt &data_f = edge.new_element("data");
622  data_f.set_attribute("key", "originfile");
623  data_f.data = id2string(graphml[from].file);
624 
625  xmlt &data_l = edge.new_element("data");
626  data_l.set_attribute("key", "startline");
627  data_l.data = id2string(graphml[from].line);
628  }
629 
630  if(
631  (it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
632  it->ssa_full_lhs.is_not_nil())
633  {
634  irep_idt identifier = it->ssa_lhs.get_object_name();
635 
636  graphml[to].has_invariant = true;
637  code_assignt assign(it->ssa_lhs, it->ssa_rhs);
638  graphml[to].invariant = convert_assign_rec(identifier, assign);
639  graphml[to].invariant_scope = id2string(it->source.function_id);
640  }
641 
642  graphml[to].in[from].xml_node = edge;
643  graphml[from].out[to].xml_node = edge;
644 
645  break;
646  }
647 
663  // ignore
664  break;
665  }
666 
667  it=next;
668  step_nr=next_step_nr;
669  }
670 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3050
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:56
goto_trace_stept::typet::LOCATION
@ LOCATION
typet::subtype
const typet & subtype() const
Definition: type.h:47
goto_trace_stept::typet::ASSUME
@ ASSUME
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
graphmlt::key_values
key_valuest key_values
Definition: graphml.h:65
arith_tools.h
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
thread_id
const std::string thread_id
Definition: java_bytecode_concurrency_instrumentation.cpp:22
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:57
data
Definition: kdev_t.h:24
pointer_predicates.h
Various predicates over pointers in programs.
prefix.h
file
Definition: kdev_t.h:19
contains_symbol_prefix
static bool contains_symbol_prefix(const exprt &expr, const std::string &prefix)
Definition: graphml_witness.cpp:261
string_container.h
Container for C-Strings.
goto_tracet::steps
stepst steps
Definition: goto_trace.h:174
grapht::add_node
node_indext add_node(arguments &&... values)
Definition: graph.h:181
exprt
Base class for all expressions.
Definition: expr.h:53
pointee_address_equalt
Functor to check whether iterators from different collections point at the same object.
Definition: goto_program.h:1164
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
mode.h
graphml_witnesst::remove_l0_l1
void remove_l0_l1(exprt &expr)
Definition: graphml_witness.cpp:39
to_array_list_expr
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition: std_expr.h:1513
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
graphml_witnesst::cache
std::unordered_map< std::pair< unsigned int, const irept::dt * >, std::string, pair_hash< unsigned int, const irept::dt * > > cache
Definition: graphml_witness.h:68
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:46
grapht< xml_graph_nodet >::node_indext
nodet::node_indext node_indext
Definition: graph.h:174
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
grapht::in
const edgest & in(node_indext n) const
Definition: graph.h:223
byte_operators.h
Expression classes for byte-level operators.
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:128
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
filter_out
static bool filter_out(const goto_tracet &goto_trace, const goto_tracet::stepst::const_iterator &prev_it, goto_tracet::stepst::const_iterator &it)
Definition: graphml_witness.cpp:219
get_mode_from_identifier
const irep_idt & get_mode_from_identifier(const namespacet &ns, const irep_idt &identifier)
Get the mode of the given identifier's symbol.
Definition: mode.cpp:65
goto_trace_stept::typet::DECL
@ DECL
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:148
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_trace_stept::typet::ASSERT
@ ASSERT
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:43
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
language_util.h
SYMEX_DYNAMIC_PREFIX
#define SYMEX_DYNAMIC_PREFIX
Definition: pointer_predicates.h:17
goto_trace_stept::typet::NONE
@ NONE
expr2c.h
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3878
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
sharing_treet::read
const dt & read() const
Definition: irep.h:270
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
goto_trace_stept::typet::ASSIGNMENT
@ ASSIGNMENT
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
graphml_witnesst::graphml
graphmlt graphml
Definition: graphml_witness.h:39
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
dstringt::empty
bool empty() const
Definition: dstring.h:88
goto_trace_stept::typet::INPUT
@ INPUT
goto_trace_stept::typet::ATOMIC_END
@ ATOMIC_END
graphml_witness.h
Witnesses for Traces and Proofs.
cprover_prefix.h
xmlt
Definition: xml.h:21
goto_trace_stept::typet::SPAWN
@ SPAWN
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3112
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
goto_program.h
Concrete Goto Program.
source_locationt
Definition: source_location.h:20
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
grapht::out
const edgest & out(node_indext n) const
Definition: graph.h:228
ssa_expr.h
goto_trace_stept::typet::GOTO
@ GOTO
graphml_witnesst::operator()
void operator()(const goto_tracet &goto_trace)
counterexample witness
Definition: graphml_witness.cpp:279
dstringt::get_no
unsigned get_no() const
Definition: dstring.h:165
array_typet
Arrays with given size.
Definition: std_types.h:965
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
symbolt
Symbol table entry.
Definition: symbol.h:28
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:257
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
graphml_witnesst::convert_assign_rec
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
Definition: graphml_witness.cpp:65
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
expr2c_configurationt::clean_configuration
static expr2c_configurationt clean_configuration
This prints compilable C that loses some of the internal details of the GOTO program.
Definition: expr2c.h:64
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
graphml_witnesst::ns
const namespacet & ns
Definition: graphml_witness.h:38
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
array_list_exprt
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1478
exprt::operands
operandst & operands()
Definition: expr.h:95
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
index_exprt
Array index operator.
Definition: std_expr.h:1293
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
xmlt::data
std::string data
Definition: xml.h:39
source_locationt::is_built_in
static bool is_built_in(const std::string &s)
Definition: source_location.cpp:16
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
expr_to_string
static std::string expr_to_string(const namespacet &ns, const irep_idt &id, const exprt &expr)
Definition: graphml_witness.cpp:31
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:866
c_types.h
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:106
validation_modet::INVARIANT
@ INVARIANT
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
goto_trace_stept::typet::DEAD
@ DEAD
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT
get_string_container
string_containert & get_string_container()
Get a reference to the global string container.
Definition: string_container.h:93