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