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->get_condition()) << '\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 
256 static void trace_value(
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_id.empty())
296  {
297  const symbolt &symbol = ns.lookup(state.function_id);
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.function_id, *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  {
391  out << " "
392  << from_expr(ns, step.function_id, step.pc->get_condition())
393  << '\n';
394  }
395 
396  out << '\n';
397  }
398  break;
399 
401  if(
402  step.assignment_type ==
404  {
405  break;
406  }
407 
408  out << " ";
409 
410  if(!step.pc->source_location.get_line().empty())
411  {
412  out << messaget::faint << step.pc->source_location.get_line() << ':'
413  << messaget::reset << ' ';
414  }
415 
416  trace_value(
417  out,
418  ns,
419  step.get_lhs_object(),
420  step.full_lhs,
421  step.full_lhs_value,
422  options);
423  break;
424 
426  // downwards arrow
427  out << '\n' << messaget::faint << u8"\u21b3" << messaget::reset << ' ';
428  if(!step.pc->source_location.get_file().empty())
429  {
430  out << messaget::faint << step.pc->source_location.get_file();
431 
432  if(!step.pc->source_location.get_line().empty())
433  {
434  out << messaget::faint << ':' << step.pc->source_location.get_line();
435  }
436 
437  out << messaget::reset << ' ';
438  }
439 
440  {
441  // show the display name
442  const auto &f_symbol = ns.lookup(step.called_function);
443  out << f_symbol.display_name();
444  }
445 
446  {
447  auto arg_strings = make_range(step.function_arguments)
448  .map([&ns, &step](const exprt &arg) {
449  return from_expr(ns, step.function_id, arg);
450  });
451 
452  out << '(';
453  join_strings(out, arg_strings.begin(), arg_strings.end(), ", ");
454  out << ")\n";
455  }
456 
457  break;
458 
460  // upwards arrow
461  out << messaget::faint << u8"\u21b5" << messaget::reset << '\n';
462  break;
463 
475  break;
476 
477  default:
478  UNREACHABLE;
479  }
480  }
481 }
482 
484  messaget::mstreamt &out,
485  const namespacet &ns,
486  const goto_tracet &goto_trace,
487  const trace_optionst &options)
488 {
489  unsigned prev_step_nr=0;
490  bool first_step=true;
491  std::size_t function_depth=0;
492 
493  for(const auto &step : goto_trace.steps)
494  {
495  // hide the hidden ones
496  if(step.hidden)
497  continue;
498 
499  switch(step.type)
500  {
502  if(!step.cond_value)
503  {
504  out << '\n';
505  out << messaget::red << "Violated property:" << messaget::reset << '\n';
506  if(!step.pc->source_location.is_nil())
507  {
508  out << " " << state_location(step, ns) << '\n';
509  }
510 
511  out << " " << messaget::red << step.comment << messaget::reset << '\n';
512 
513  if(step.pc->is_assert())
514  {
515  out << " "
516  << from_expr(ns, step.function_id, step.pc->get_condition())
517  << '\n';
518  }
519 
520  out << '\n';
521  }
522  break;
523 
525  if(step.cond_value && step.pc->is_assume())
526  {
527  out << "\n";
528  out << "Assumption:\n";
529 
530  if(!step.pc->source_location.is_nil())
531  out << " " << step.pc->source_location << '\n';
532 
533  out << " " << from_expr(ns, step.function_id, step.pc->get_condition())
534  << '\n';
535  }
536  break;
537 
539  break;
540 
542  break;
543 
545  if(step.pc->is_assign() ||
546  step.pc->is_return() || // returns have a lhs!
547  step.pc->is_function_call() ||
548  (step.pc->is_other() && step.full_lhs.is_not_nil()))
549  {
550  if(prev_step_nr!=step.step_nr || first_step)
551  {
552  first_step=false;
553  prev_step_nr=step.step_nr;
554  show_state_header(out, ns, step, step.step_nr, options);
555  }
556 
557  out << " ";
558  trace_value(
559  out,
560  ns,
561  step.get_lhs_object(),
562  step.full_lhs,
563  step.full_lhs_value,
564  options);
565  }
566  break;
567 
569  if(prev_step_nr!=step.step_nr || first_step)
570  {
571  first_step=false;
572  prev_step_nr=step.step_nr;
573  show_state_header(out, ns, step, step.step_nr, options);
574  }
575 
576  out << " ";
577  trace_value(
578  out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
579  break;
580 
582  if(step.formatted)
583  {
584  printf_formattert printf_formatter(ns);
585  printf_formatter(id2string(step.format_string), step.io_args);
586  printf_formatter.print(out);
587  out << '\n';
588  }
589  else
590  {
591  show_state_header(out, ns, step, step.step_nr, options);
592  out << " OUTPUT " << step.io_id << ':';
593 
594  for(std::list<exprt>::const_iterator
595  l_it=step.io_args.begin();
596  l_it!=step.io_args.end();
597  l_it++)
598  {
599  if(l_it!=step.io_args.begin())
600  out << ';';
601 
602  out << ' ' << from_expr(ns, step.function_id, *l_it);
603 
604  // the binary representation
605  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
606  }
607 
608  out << '\n';
609  }
610  break;
611 
613  show_state_header(out, ns, step, step.step_nr, options);
614  out << " INPUT " << step.io_id << ':';
615 
616  for(std::list<exprt>::const_iterator
617  l_it=step.io_args.begin();
618  l_it!=step.io_args.end();
619  l_it++)
620  {
621  if(l_it!=step.io_args.begin())
622  out << ';';
623 
624  out << ' ' << from_expr(ns, step.function_id, *l_it);
625 
626  // the binary representation
627  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
628  }
629 
630  out << '\n';
631  break;
632 
634  function_depth++;
635  if(options.show_function_calls)
636  {
637  out << "\n#### Function call: " << step.called_function;
638  out << '(';
639 
640  bool first = true;
641  for(auto &arg : step.function_arguments)
642  {
643  if(first)
644  first = false;
645  else
646  out << ", ";
647 
648  out << from_expr(ns, step.function_id, arg);
649  }
650 
651  out << ") (depth " << function_depth << ") ####\n";
652  }
653  break;
654 
656  function_depth--;
657  if(options.show_function_calls)
658  {
659  out << "\n#### Function return from " << step.function_id << " (depth "
660  << function_depth << ") ####\n";
661  }
662  break;
663 
669  break;
670 
674  default:
675  UNREACHABLE;
676  }
677  }
678 }
679 
681  messaget::mstreamt &out,
682  const namespacet &ns,
683  const goto_tracet &goto_trace)
684 {
685  // map from thread number to a call stack
686  std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
687  call_stacks;
688 
689  // by default, we show thread 0
690  unsigned thread_to_show = 0;
691 
692  for(auto s_it = goto_trace.steps.begin(); s_it != goto_trace.steps.end();
693  s_it++)
694  {
695  const auto &step = *s_it;
696  auto &stack = call_stacks[step.thread_nr];
697 
698  if(step.is_assert())
699  {
700  if(!step.cond_value)
701  {
702  stack.push_back(s_it);
703  thread_to_show = step.thread_nr;
704  }
705  }
706  else if(step.is_function_call())
707  {
708  stack.push_back(s_it);
709  }
710  else if(step.is_function_return())
711  {
712  stack.pop_back();
713  }
714  }
715 
716  const auto &stack = call_stacks[thread_to_show];
717 
718  // print in reverse order
719  for(auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
720  {
721  const auto &step = **s_it;
722  if(step.is_assert())
723  {
724  out << " assertion failure";
725  if(!step.pc->source_location.is_nil())
726  out << ' ' << step.pc->source_location;
727  out << '\n';
728  }
729  else if(step.is_function_call())
730  {
731  out << " " << step.called_function;
732  out << '(';
733 
734  bool first = true;
735  for(auto &arg : step.function_arguments)
736  {
737  if(first)
738  first = false;
739  else
740  out << ", ";
741 
742  out << from_expr(ns, step.function_id, arg);
743  }
744 
745  out << ')';
746 
747  if(!step.pc->source_location.is_nil())
748  out << ' ' << step.pc->source_location;
749 
750  out << '\n';
751  }
752  }
753 }
754 
756  messaget::mstreamt &out,
757  const namespacet &ns,
758  const goto_tracet &goto_trace,
759  const trace_optionst &options)
760 {
761  if(options.stack_trace)
762  show_goto_stack_trace(out, ns, goto_trace);
763  else if(options.compact_trace)
764  show_compact_goto_trace(out, ns, goto_trace, options);
765  else
766  show_full_goto_trace(out, ns, goto_trace, options);
767 }
768 
770 
771 std::set<irep_idt> goto_tracet::get_failed_property_ids() const
772 {
773  std::set<irep_idt> property_ids;
774  for(const auto &step : steps)
775  {
776  if(step.is_assert() && !step.cond_value)
777  property_ids.insert(step.property_id);
778  }
779  return property_ids;
780 }
The type of an expression, extends irept.
Definition: type.h:28
BigInt mp_integer
Definition: mp_arith.h:20
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Output the trace on the given stream out.
Definition: goto_trace.cpp:755
bool is_nil() const
Definition: irep.h:393
const std::string & id2string(const irep_idt &d)
Definition: irep.h:42
Symbol table entry.
bool show_function_calls
Show function calls in plain text trace.
Definition: goto_trace.h:224
bool is_goto() const
Definition: goto_trace.h:58
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
bool base_prefix
Use prefix (0b or 0x) for distinguishing the base of the representation.
Definition: goto_trace.h:222
uint64_t u8
Definition: bytecode_info.h:58
exprt & op0()
Definition: expr.h:91
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1093
const exprt & op() const
Definition: std_expr.h:337
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:4286
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:75
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:4266
Step of the trace of a GOTO program.
Definition: goto_trace.h:49
stepst steps
Definition: goto_trace.h:174
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:324
goto_programt::const_targett pc
Definition: goto_trace.h:112
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:141
std::set< irep_idt > get_failed_property_ids() const
Returns the property IDs of all failed assertions in the trace.
Definition: goto_trace.cpp:771
bool stack_trace
Give a stack trace only.
Definition: goto_trace.h:230
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:214
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:60
const irep_idt & id() const
Definition: irep.h:413
bool is_index_member_symbol(const exprt &src)
Definition: goto_trace.cpp:341
bool is_assume() const
Definition: goto_trace.h:56
static std::string state_location(const goto_trace_stept &state, const namespacet &ns)
Definition: goto_trace.cpp:286
bool show_code
Show original code in plain text trace.
Definition: goto_trace.h:226
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:239
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:130
unsigned thread_nr
Definition: goto_trace.h:115
static const commandt red
render text with red foreground color
Definition: message.h:327
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
std::string as_string(resultt result)
Definition: properties.cpp:20
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3841
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:42
#define forall_operands(it, expr)
Definition: expr.h:18
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:227
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:58
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:393
bool hex_representation
Represent plain trace values in hex.
Definition: goto_trace.h:219
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:36
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4311
std::size_t get_width() const
Definition: std_types.h:1052
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:722
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
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:366
bool compact_trace
Give a compact trace.
Definition: goto_trace.h:228
static 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
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:483
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:52
const exprt & struct_op() const
Definition: std_expr.h:3787
exprt full_lhs_value
Definition: goto_trace.h:132
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:2289
void print(std::ostream &out)
std::string comment
Definition: goto_trace.h:123
irep_idt function_id
Definition: goto_trace.h:111
bool is_assert() const
Definition: goto_trace.h:57
bool is_assignment() const
Definition: goto_trace.h:55
static void show_goto_stack_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:680
Trace of a GOTO program.
Definition: goto_trace.h:170
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:232
const typet & subtype() const
Definition: type.h:40
operandst & operands()
Definition: expr.h:85
#define stack(x)
Definition: parser.h:144
bool empty() const
Definition: dstring.h:88
exprt & array()
Definition: std_expr.h:1518
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1556
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
static format_containert< T > format(const T &o)
Definition: format.h:35