cprover
goto_trace.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Traces of GOTO Programs
4 
5 Author: Daniel Kroening
6 
7  Date: July 2005
8 
9 \*******************************************************************/
10 
13 
14 #include "goto_trace.h"
15 
16 #include <ostream>
17 
18 #include <util/arith_tools.h>
19 #include <util/format_expr.h>
20 #include <util/range.h>
21 #include <util/string_utils.h>
22 #include <util/symbol.h>
23 
24 #include <langapi/language_util.h>
25 
26 #include "printf_formatter.h"
27 
29 {
30  if(src.id()==ID_symbol)
31  return to_symbol_expr(src);
32  else if(src.id()==ID_member)
34  else if(src.id()==ID_index)
35  return get_object_rec(to_index_expr(src).array());
36  else if(src.id()==ID_typecast)
37  return get_object_rec(to_typecast_expr(src).op());
38  else
39  return {}; // give up
40 }
41 
43 {
44  return get_object_rec(full_lhs);
45 }
46 
48  const class namespacet &ns,
49  std::ostream &out) const
50 {
51  for(const auto &step : steps)
52  step.output(ns, out);
53 }
54 
56  const namespacet &,
57  std::ostream &out) const
58 {
59  out << "*** ";
60 
61  switch(type)
62  {
63  case goto_trace_stept::typet::ASSERT: out << "ASSERT"; break;
64  case goto_trace_stept::typet::ASSUME: out << "ASSUME"; break;
65  case goto_trace_stept::typet::LOCATION: out << "LOCATION"; break;
66  case goto_trace_stept::typet::ASSIGNMENT: out << "ASSIGNMENT"; break;
67  case goto_trace_stept::typet::GOTO: out << "GOTO"; break;
68  case goto_trace_stept::typet::DECL: out << "DECL"; break;
69  case goto_trace_stept::typet::DEAD: out << "DEAD"; break;
70  case goto_trace_stept::typet::OUTPUT: out << "OUTPUT"; break;
71  case goto_trace_stept::typet::INPUT: out << "INPUT"; break;
73  out << "ATOMIC_BEGIN";
74  break;
75  case goto_trace_stept::typet::ATOMIC_END: out << "ATOMIC_END"; break;
76  case goto_trace_stept::typet::SHARED_READ: out << "SHARED_READ"; break;
77  case goto_trace_stept::typet::SHARED_WRITE: out << "SHARED WRITE"; break;
78  case goto_trace_stept::typet::FUNCTION_CALL: out << "FUNCTION CALL"; break;
80  out << "FUNCTION RETURN"; break;
81  default:
82  out << "unknown type: " << static_cast<int>(type) << std::endl;
84  }
85 
86  if(is_assert() || is_assume() || is_goto())
87  out << " (" << cond_value << ')';
88  else if(is_function_call())
89  out << ' ' << called_function;
90 
91  if(hidden)
92  out << " hidden";
93 
94  out << '\n';
95 
96  if(is_assignment())
97  {
98  out << " " << format(full_lhs)
99  << " = " << format(full_lhs_value)
100  << '\n';
101  }
102 
103  if(!pc->source_location.is_nil())
104  out << pc->source_location << '\n';
105 
106  out << pc->type << '\n';
107 
108  if(pc->is_assert())
109  {
110  if(!cond_value)
111  {
112  out << "Violated property:" << '\n';
113  if(pc->source_location.is_nil())
114  out << " " << pc->source_location << '\n';
115 
116  if(!comment.empty())
117  out << " " << comment << '\n';
118 
119  out << " " << format(pc->guard) << '\n';
120  out << '\n';
121  }
122  }
123 
124  out << '\n';
125 }
135 static std::string numeric_representation(
136  const constant_exprt &expr,
137  const namespacet &ns,
138  const trace_optionst &options)
139 {
140  std::string result;
141  std::string prefix;
142 
143  const typet &expr_type = expr.type();
144 
145  const typet &underlying_type =
146  expr_type.id() == ID_c_enum_tag
147  ? ns.follow_tag(to_c_enum_tag_type(expr_type)).subtype()
148  : expr_type;
149 
150  const irep_idt &value = expr.get_value();
151 
152  const auto width = to_bitvector_type(underlying_type).get_width();
153 
154  const mp_integer value_int = bvrep2integer(id2string(value), width, false);
155 
156  if(options.hex_representation)
157  {
158  result = integer2string(value_int, 16);
159  prefix = "0x";
160  }
161  else
162  {
163  result = integer2binary(value_int, width);
164  prefix = "0b";
165  }
166 
167  std::ostringstream oss;
169  for(const auto c : result)
170  {
171  oss << c;
172  if(++i % 8 == 0 && result.size() != i)
173  oss << ' ';
174  }
175  if(options.base_prefix)
176  return prefix + oss.str();
177  else
178  return oss.str();
179 }
180 
182  const exprt &expr,
183  const namespacet &ns,
184  const trace_optionst &options)
185 {
186  const typet &type = expr.type();
187 
188  if(expr.id()==ID_constant)
189  {
190  if(type.id()==ID_unsignedbv ||
191  type.id()==ID_signedbv ||
192  type.id()==ID_bv ||
193  type.id()==ID_fixedbv ||
194  type.id()==ID_floatbv ||
195  type.id()==ID_pointer ||
196  type.id()==ID_c_bit_field ||
197  type.id()==ID_c_bool ||
198  type.id()==ID_c_enum ||
199  type.id()==ID_c_enum_tag)
200  {
201  return numeric_representation(to_constant_expr(expr), ns, options);
202  }
203  else if(type.id()==ID_bool)
204  {
205  return expr.is_true()?"1":"0";
206  }
207  else if(type.id()==ID_integer)
208  {
209  const auto i = numeric_cast<mp_integer>(expr);
210  if(i.has_value() && *i >= 0)
211  {
212  if(options.hex_representation)
213  return "0x" + integer2string(*i, 16);
214  else
215  return "0b" + integer2string(*i, 2);
216  }
217  }
218  }
219  else if(expr.id()==ID_array)
220  {
221  std::string result;
222 
223  forall_operands(it, expr)
224  {
225  if(result=="")
226  result="{ ";
227  else
228  result+=", ";
229  result+=trace_numeric_value(*it, ns, options);
230  }
231 
232  return result+" }";
233  }
234  else if(expr.id()==ID_struct)
235  {
236  std::string result="{ ";
237 
238  forall_operands(it, expr)
239  {
240  if(it!=expr.operands().begin())
241  result+=", ";
242  result+=trace_numeric_value(*it, ns, options);
243  }
244 
245  return result+" }";
246  }
247  else if(expr.id()==ID_union)
248  {
249  PRECONDITION(expr.operands().size()==1);
250  return trace_numeric_value(expr.op0(), ns, options);
251  }
252 
253  return "?";
254 }
255 
257  messaget::mstreamt &out,
258  const namespacet &ns,
259  const optionalt<symbol_exprt> &lhs_object,
260  const exprt &full_lhs,
261  const exprt &value,
262  const trace_optionst &options)
263 {
264  irep_idt identifier;
265 
266  if(lhs_object.has_value())
267  identifier=lhs_object->get_identifier();
268 
269  out << from_expr(ns, identifier, full_lhs) << '=';
270 
271  if(value.is_nil())
272  out << "(assignment removed)";
273  else
274  {
275  out << from_expr(ns, identifier, value);
276 
277  // the binary representation
278  out << ' ' << messaget::faint << '('
279  << trace_numeric_value(value, ns, options) << ')' << messaget::reset;
280  }
281 
282  out << '\n';
283 }
284 
285 static std::string
287 {
288  std::string result;
289 
290  const auto &source_location = state.pc->source_location;
291 
292  if(!source_location.get_file().empty())
293  result += "file " + id2string(source_location.get_file());
294 
295  if(!state.function.empty())
296  {
297  const symbolt &symbol = ns.lookup(state.function);
298  if(!result.empty())
299  result += ' ';
300  result += "function " + id2string(symbol.display_name());
301  }
302 
303  if(!source_location.get_line().empty())
304  {
305  if(!result.empty())
306  result += ' ';
307  result += "line " + id2string(source_location.get_line());
308  }
309 
310  if(!result.empty())
311  result += ' ';
312  result += "thread " + std::to_string(state.thread_nr);
313 
314  return result;
315 }
316 
318  messaget::mstreamt &out,
319  const namespacet &ns,
320  const goto_trace_stept &state,
321  unsigned step_nr,
322  const trace_optionst &options)
323 {
324  out << '\n';
325 
326  if(step_nr == 0)
327  out << "Initial State";
328  else
329  out << "State " << step_nr;
330 
331  out << ' ' << state_location(state, ns) << '\n';
332  out << "----------------------------------------------------" << '\n';
333 
334  if(options.show_code)
335  {
336  out << as_string(ns, *state.pc) << '\n';
337  out << "----------------------------------------------------" << '\n';
338  }
339 }
340 
342 {
343  if(src.id()==ID_index)
344  return is_index_member_symbol(src.op0());
345  else if(src.id()==ID_member)
346  return is_index_member_symbol(src.op0());
347  else if(src.id()==ID_symbol)
348  return true;
349  else
350  return false;
351 }
352 
359  messaget::mstreamt &out,
360  const namespacet &ns,
361  const goto_tracet &goto_trace,
362  const trace_optionst &options)
363 {
364  std::size_t function_depth = 0;
365 
366  for(const auto &step : goto_trace.steps)
367  {
368  if(step.is_function_call())
369  function_depth++;
370  else if(step.is_function_return())
371  function_depth--;
372 
373  // hide the hidden ones
374  if(step.hidden)
375  continue;
376 
377  switch(step.type)
378  {
380  if(!step.cond_value)
381  {
382  out << '\n';
383  out << messaget::red << "Violated property:" << messaget::reset << '\n';
384  if(!step.pc->source_location.is_nil())
385  out << " " << state_location(step, ns) << '\n';
386 
387  out << " " << messaget::red << step.comment << messaget::reset << '\n';
388 
389  if(step.pc->is_assert())
390  out << " " << from_expr(ns, step.function, step.pc->guard) << '\n';
391 
392  out << '\n';
393  }
394  break;
395 
397  if(
398  step.assignment_type ==
400  {
401  break;
402  }
403 
404  out << " ";
405 
406  if(!step.pc->source_location.get_line().empty())
407  {
408  out << messaget::faint << step.pc->source_location.get_line() << ':'
409  << messaget::reset << ' ';
410  }
411 
412  trace_value(
413  out,
414  ns,
415  step.get_lhs_object(),
416  step.full_lhs,
417  step.full_lhs_value,
418  options);
419  break;
420 
422  // downwards arrow
423  out << '\n' << messaget::faint << u8"\u21b3" << messaget::reset << ' ';
424  if(!step.pc->source_location.get_file().empty())
425  {
426  out << messaget::faint << step.pc->source_location.get_file();
427 
428  if(!step.pc->source_location.get_line().empty())
429  {
430  out << messaget::faint << ':' << step.pc->source_location.get_line();
431  }
432 
433  out << messaget::reset << ' ';
434  }
435 
436  {
437  // show the display name
438  const auto &f_symbol = ns.lookup(step.called_function);
439  out << f_symbol.display_name();
440  }
441 
442  {
443  auto arg_strings = make_range(step.function_arguments)
444  .map([&ns, &step](const exprt &arg) {
445  return from_expr(ns, step.function, arg);
446  });
447 
448  out << '(';
449  join_strings(out, arg_strings.begin(), arg_strings.end(), ", ");
450  out << ")\n";
451  }
452 
453  break;
454 
456  // upwards arrow
457  out << messaget::faint << u8"\u21b5" << messaget::reset << '\n';
458  break;
459 
471  break;
472 
473  default:
474  UNREACHABLE;
475  }
476  }
477 }
478 
480  messaget::mstreamt &out,
481  const namespacet &ns,
482  const goto_tracet &goto_trace,
483  const trace_optionst &options)
484 {
485  unsigned prev_step_nr=0;
486  bool first_step=true;
487  std::size_t function_depth=0;
488 
489  for(const auto &step : goto_trace.steps)
490  {
491  // hide the hidden ones
492  if(step.hidden)
493  continue;
494 
495  switch(step.type)
496  {
498  if(!step.cond_value)
499  {
500  out << '\n';
501  out << messaget::red << "Violated property:" << messaget::reset << '\n';
502  if(!step.pc->source_location.is_nil())
503  {
504  out << " " << state_location(step, ns) << '\n';
505  }
506 
507  out << " " << messaget::red << step.comment << messaget::reset << '\n';
508 
509  if(step.pc->is_assert())
510  out << " " << from_expr(ns, step.function, step.pc->guard) << '\n';
511 
512  out << '\n';
513  }
514  break;
515 
517  if(!step.cond_value)
518  {
519  out << '\n';
520  out << "Violated assumption:" << '\n';
521  if(!step.pc->source_location.is_nil())
522  out << " " << step.pc->source_location << '\n';
523 
524  if(step.pc->is_assume())
525  out << " " << from_expr(ns, step.function, step.pc->guard) << '\n';
526 
527  out << '\n';
528  }
529  break;
530 
532  break;
533 
535  break;
536 
538  if(step.pc->is_assign() ||
539  step.pc->is_return() || // returns have a lhs!
540  step.pc->is_function_call() ||
541  (step.pc->is_other() && step.full_lhs.is_not_nil()))
542  {
543  if(prev_step_nr!=step.step_nr || first_step)
544  {
545  first_step=false;
546  prev_step_nr=step.step_nr;
547  show_state_header(out, ns, step, step.step_nr, options);
548  }
549 
550  out << " ";
551  trace_value(
552  out,
553  ns,
554  step.get_lhs_object(),
555  step.full_lhs,
556  step.full_lhs_value,
557  options);
558  }
559  break;
560 
562  if(prev_step_nr!=step.step_nr || first_step)
563  {
564  first_step=false;
565  prev_step_nr=step.step_nr;
566  show_state_header(out, ns, step, step.step_nr, options);
567  }
568 
569  out << " ";
570  trace_value(
571  out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
572  break;
573 
575  if(step.formatted)
576  {
577  printf_formattert printf_formatter(ns);
578  printf_formatter(id2string(step.format_string), step.io_args);
579  printf_formatter.print(out);
580  out << '\n';
581  }
582  else
583  {
584  show_state_header(out, ns, step, step.step_nr, options);
585  out << " OUTPUT " << step.io_id << ':';
586 
587  for(std::list<exprt>::const_iterator
588  l_it=step.io_args.begin();
589  l_it!=step.io_args.end();
590  l_it++)
591  {
592  if(l_it!=step.io_args.begin())
593  out << ';';
594 
595  out << ' ' << from_expr(ns, step.function, *l_it);
596 
597  // the binary representation
598  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
599  }
600 
601  out << '\n';
602  }
603  break;
604 
606  show_state_header(out, ns, step, step.step_nr, options);
607  out << " INPUT " << step.io_id << ':';
608 
609  for(std::list<exprt>::const_iterator
610  l_it=step.io_args.begin();
611  l_it!=step.io_args.end();
612  l_it++)
613  {
614  if(l_it!=step.io_args.begin())
615  out << ';';
616 
617  out << ' ' << from_expr(ns, step.function, *l_it);
618 
619  // the binary representation
620  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
621  }
622 
623  out << '\n';
624  break;
625 
627  function_depth++;
628  if(options.show_function_calls)
629  {
630  out << "\n#### Function call: " << step.called_function;
631  out << '(';
632 
633  bool first = true;
634  for(auto &arg : step.function_arguments)
635  {
636  if(first)
637  first = false;
638  else
639  out << ", ";
640 
641  out << from_expr(ns, step.function, arg);
642  }
643 
644  out << ") (depth " << function_depth << ") ####\n";
645  }
646  break;
647 
649  function_depth--;
650  if(options.show_function_calls)
651  {
652  out << "\n#### Function return from " << step.function << " (depth "
653  << function_depth << ") ####\n";
654  }
655  break;
656 
662  break;
663 
667  default:
668  UNREACHABLE;
669  }
670  }
671 }
672 
674  messaget::mstreamt &out,
675  const namespacet &ns,
676  const goto_tracet &goto_trace)
677 {
678  // map from thread number to a call stack
679  std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
680  call_stacks;
681 
682  // by default, we show thread 0
683  unsigned thread_to_show = 0;
684 
685  for(auto s_it = goto_trace.steps.begin(); s_it != goto_trace.steps.end();
686  s_it++)
687  {
688  const auto &step = *s_it;
689  auto &stack = call_stacks[step.thread_nr];
690 
691  if(step.is_assert())
692  {
693  if(!step.cond_value)
694  {
695  stack.push_back(s_it);
696  thread_to_show = step.thread_nr;
697  }
698  }
699  else if(step.is_function_call())
700  {
701  stack.push_back(s_it);
702  }
703  else if(step.is_function_return())
704  {
705  stack.pop_back();
706  }
707  }
708 
709  const auto &stack = call_stacks[thread_to_show];
710 
711  // print in reverse order
712  for(auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
713  {
714  const auto &step = **s_it;
715  if(step.is_assert())
716  {
717  out << " assertion failure";
718  if(!step.pc->source_location.is_nil())
719  out << ' ' << step.pc->source_location;
720  out << '\n';
721  }
722  else if(step.is_function_call())
723  {
724  out << " " << step.called_function;
725  out << '(';
726 
727  bool first = true;
728  for(auto &arg : step.function_arguments)
729  {
730  if(first)
731  first = false;
732  else
733  out << ", ";
734 
735  out << from_expr(ns, step.function, arg);
736  }
737 
738  out << ')';
739 
740  if(!step.pc->source_location.is_nil())
741  out << ' ' << step.pc->source_location;
742 
743  out << '\n';
744  }
745  }
746 }
747 
749  messaget::mstreamt &out,
750  const namespacet &ns,
751  const goto_tracet &goto_trace,
752  const trace_optionst &options)
753 {
754  if(options.stack_trace)
755  show_goto_stack_trace(out, ns, goto_trace);
756  else if(options.compact_trace)
757  show_compact_goto_trace(out, ns, goto_trace, options);
758  else
759  show_full_goto_trace(out, ns, goto_trace, options);
760 }
761 
763  messaget::mstreamt &out,
764  const namespacet &ns,
765  const goto_tracet &goto_trace)
766 {
767  show_goto_trace(out, ns, goto_trace, trace_optionst::default_options);
768 }
769 
The type of an expression, extends irept.
Definition: type.h:27
BigInt mp_integer
Definition: mp_arith.h:22
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Definition: goto_trace.cpp:748
bool is_nil() const
Definition: irep.h:169
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Symbol table entry.
bool show_function_calls
Definition: goto_trace.h:201
bool is_goto() const
Definition: goto_trace.h:38
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
uint64_t u8
Definition: bytecode_info.h:58
exprt & op0()
Definition: expr.h:84
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1143
const exprt & op() const
Definition: std_expr.h:382
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::string trace_numeric_value(const exprt &expr, const namespacet &ns, const trace_optionst &options)
Definition: goto_trace.cpp:181
void show_state_header(messaget::mstreamt &out, const namespacet &ns, const goto_trace_stept &state, unsigned step_nr, const trace_optionst &options)
Definition: goto_trace.cpp:317
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const irep_idt & get_value() const
Definition: std_expr.h:4458
Traces of GOTO Programs.
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
typet & type()
Return the type of the expression.
Definition: expr.h:68
unsignedbv_typet size_type()
Definition: c_types.cpp:58
Symbol table entry.
Definition: symbol.h:27
printf Formatting
A constant literal expression.
Definition: std_expr.h:4439
TO_BE_DOCUMENTED.
Definition: goto_trace.h:30
stepst steps
Definition: goto_trace.h:154
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:331
goto_programt::const_targett pc
Definition: goto_trace.h:92
Stream & join_strings(Stream &os, const It b, const It e, const Delimiter &delimiter)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:52
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace in ASCII to a given stream
Definition: goto_trace.cpp:47
irep_idt called_function
Definition: goto_trace.h:120
irep_idt function
Definition: goto_trace.h:91
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace step in ASCII to a given stream
Definition: goto_trace.cpp:55
bool is_function_call() const
Definition: goto_trace.h:40
const irep_idt & id() const
Definition: irep.h:256
bool is_index_member_symbol(const exprt &src)
Definition: goto_trace.cpp:341
bool is_assume() const
Definition: goto_trace.h:36
static std::string state_location(const goto_trace_stept &state, const namespacet &ns)
Definition: goto_trace.cpp:286
Ranges: pair of begin and end iterators, which can be initialized from containers, provide useful methods such as map, filter and concat which only manipulate iterators, and can be used with ranged-for.
source_locationt source_location
Definition: message.h:237
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:123
unsigned thread_nr
Definition: goto_trace.h:95
static const commandt red
render text with red foreground color
Definition: message.h:334
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
std::string as_string(resultt result)
Definition: properties.cpp:19
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:4014
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:42
#define forall_operands(it, expr)
Definition: expr.h:20
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:262
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:384
bool hex_representation
Definition: goto_trace.h:199
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4478
std::size_t get_width() const
Definition: std_types.h:1102
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:761
void trace_value(messaget::mstreamt &out, const namespacet &ns, const optionalt< symbol_exprt > &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &options)
Definition: goto_trace.cpp:256
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
static const commandt faint
render text with faint font
Definition: message.h:373
bool compact_trace
Definition: goto_trace.h:203
void show_compact_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
show a compact variant of the goto trace on the console
Definition: goto_trace.cpp:358
void show_full_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Definition: goto_trace.cpp:479
static std::string numeric_representation(const constant_exprt &expr, const namespacet &ns, const trace_optionst &options)
Returns the numeric representation of an expression, based on options.
Definition: goto_trace.cpp:135
Base class for all expressions.
Definition: expr.h:54
const exprt & struct_op() const
Definition: std_expr.h:3986
exprt full_lhs_value
Definition: goto_trace.h:111
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2341
void print(std::ostream &out)
std::string comment
Definition: goto_trace.h:102
bool is_assert() const
Definition: goto_trace.h:37
bool is_assignment() const
Definition: goto_trace.h:35
static void show_goto_stack_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:673
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
static optionalt< symbol_exprt > get_object_rec(const exprt &src)
Definition: goto_trace.cpp:28
static const trace_optionst default_options
Definition: goto_trace.h:206
const typet & subtype() const
Definition: type.h:38
operandst & operands()
Definition: expr.h:78
#define stack(x)
Definition: parser.h:144
bool empty() const
Definition: dstring.h:75
exprt & array()
Definition: std_expr.h:1637
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1664
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:165
static format_containert< T > format(const T &o)
Definition: format.h:35