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