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/byte_operators.h>
20 #include <util/format_expr.h>
21 #include <util/range.h>
22 #include <util/string_utils.h>
23 #include <util/symbol.h>
24 
25 #include <langapi/language_util.h>
26 
27 #include "printf_formatter.h"
28 
30 {
31  if(src.id()==ID_symbol)
32  return to_symbol_expr(src);
33  else if(src.id()==ID_member)
35  else if(src.id()==ID_index)
36  return get_object_rec(to_index_expr(src).array());
37  else if(src.id()==ID_typecast)
38  return get_object_rec(to_typecast_expr(src).op());
39  else if(
40  src.id() == ID_byte_extract_little_endian ||
41  src.id() == ID_byte_extract_big_endian)
42  {
43  return get_object_rec(to_byte_extract_expr(src).op());
44  }
45  else
46  return {}; // give up
47 }
48 
50 {
51  return get_object_rec(full_lhs);
52 }
53 
55  const class namespacet &ns,
56  std::ostream &out) const
57 {
58  for(const auto &step : steps)
59  step.output(ns, out);
60 }
61 
63  const namespacet &,
64  std::ostream &out) const
65 {
66  out << "*** ";
67 
68  // clang-format off
69  switch(type)
70  {
71  case goto_trace_stept::typet::ASSERT: out << "ASSERT"; break;
72  case goto_trace_stept::typet::ASSUME: out << "ASSUME"; break;
73  case goto_trace_stept::typet::LOCATION: out << "LOCATION"; break;
74  case goto_trace_stept::typet::ASSIGNMENT: out << "ASSIGNMENT"; break;
75  case goto_trace_stept::typet::GOTO: out << "GOTO"; break;
76  case goto_trace_stept::typet::DECL: out << "DECL"; break;
77  case goto_trace_stept::typet::DEAD: out << "DEAD"; break;
78  case goto_trace_stept::typet::OUTPUT: out << "OUTPUT"; break;
79  case goto_trace_stept::typet::INPUT: out << "INPUT"; break;
81  out << "ATOMIC_BEGIN";
82  break;
83  case goto_trace_stept::typet::ATOMIC_END: out << "ATOMIC_END"; break;
84  case goto_trace_stept::typet::SHARED_READ: out << "SHARED_READ"; break;
85  case goto_trace_stept::typet::SHARED_WRITE: out << "SHARED WRITE"; break;
86  case goto_trace_stept::typet::FUNCTION_CALL: out << "FUNCTION CALL"; break;
88  out << "FUNCTION RETURN"; break;
89  case goto_trace_stept::typet::MEMORY_BARRIER: out << "MEMORY_BARRIER"; break;
90  case goto_trace_stept::typet::SPAWN: out << "SPAWN"; break;
91  case goto_trace_stept::typet::CONSTRAINT: out << "CONSTRAINT"; break;
92  case goto_trace_stept::typet::NONE: out << "NONE"; break;
93  }
94  // clang-format on
95 
96  if(is_assert() || is_assume() || is_goto())
97  out << " (" << cond_value << ')';
98  else if(is_function_call())
99  out << ' ' << called_function;
100 
101  if(hidden)
102  out << " hidden";
103 
104  out << '\n';
105 
106  if(is_assignment())
107  {
108  out << " " << format(full_lhs)
109  << " = " << format(full_lhs_value)
110  << '\n';
111  }
112 
113  if(!pc->source_location.is_nil())
114  out << pc->source_location << '\n';
115 
116  out << pc->type << '\n';
117 
118  if(pc->is_assert())
119  {
120  if(!cond_value)
121  {
122  out << "Violated property:" << '\n';
123  if(pc->source_location.is_nil())
124  out << " " << pc->source_location << '\n';
125 
126  if(!comment.empty())
127  out << " " << comment << '\n';
128 
129  out << " " << format(pc->get_condition()) << '\n';
130  out << '\n';
131  }
132  }
133 
134  out << '\n';
135 }
145 static std::string numeric_representation(
146  const constant_exprt &expr,
147  const namespacet &ns,
148  const trace_optionst &options)
149 {
150  std::string result;
151  std::string prefix;
152 
153  const typet &expr_type = expr.type();
154 
155  const typet &underlying_type =
156  expr_type.id() == ID_c_enum_tag
157  ? ns.follow_tag(to_c_enum_tag_type(expr_type)).subtype()
158  : expr_type;
159 
160  const irep_idt &value = expr.get_value();
161 
162  const auto width = to_bitvector_type(underlying_type).get_width();
163 
164  const mp_integer value_int = bvrep2integer(id2string(value), width, false);
165 
166  if(options.hex_representation)
167  {
168  result = integer2string(value_int, 16);
169  prefix = "0x";
170  }
171  else
172  {
173  result = integer2binary(value_int, width);
174  prefix = "0b";
175  }
176 
177  std::ostringstream oss;
179  for(const auto c : result)
180  {
181  oss << c;
182  if(++i % 8 == 0 && result.size() != i)
183  oss << ' ';
184  }
185  if(options.base_prefix)
186  return prefix + oss.str();
187  else
188  return oss.str();
189 }
190 
192  const exprt &expr,
193  const namespacet &ns,
194  const trace_optionst &options)
195 {
196  const typet &type = expr.type();
197 
198  if(expr.id()==ID_constant)
199  {
200  if(type.id()==ID_unsignedbv ||
201  type.id()==ID_signedbv ||
202  type.id()==ID_bv ||
203  type.id()==ID_fixedbv ||
204  type.id()==ID_floatbv ||
205  type.id()==ID_pointer ||
206  type.id()==ID_c_bit_field ||
207  type.id()==ID_c_bool ||
208  type.id()==ID_c_enum ||
209  type.id()==ID_c_enum_tag)
210  {
211  return numeric_representation(to_constant_expr(expr), ns, options);
212  }
213  else if(type.id()==ID_bool)
214  {
215  return expr.is_true()?"1":"0";
216  }
217  else if(type.id()==ID_integer)
218  {
219  const auto i = numeric_cast<mp_integer>(expr);
220  if(i.has_value() && *i >= 0)
221  {
222  if(options.hex_representation)
223  return "0x" + integer2string(*i, 16);
224  else
225  return "0b" + integer2string(*i, 2);
226  }
227  }
228  }
229  else if(expr.id()==ID_array)
230  {
231  std::string result;
232 
233  forall_operands(it, expr)
234  {
235  if(result.empty())
236  result="{ ";
237  else
238  result+=", ";
239  result+=trace_numeric_value(*it, ns, options);
240  }
241 
242  return result+" }";
243  }
244  else if(expr.id()==ID_struct)
245  {
246  std::string result="{ ";
247 
248  forall_operands(it, expr)
249  {
250  if(it!=expr.operands().begin())
251  result+=", ";
252  result+=trace_numeric_value(*it, ns, options);
253  }
254 
255  return result+" }";
256  }
257  else if(expr.id()==ID_union)
258  {
259  PRECONDITION(expr.operands().size()==1);
260  return trace_numeric_value(expr.op0(), ns, options);
261  }
262 
263  return "?";
264 }
265 
266 static void trace_value(
267  messaget::mstreamt &out,
268  const namespacet &ns,
269  const optionalt<symbol_exprt> &lhs_object,
270  const exprt &full_lhs,
271  const exprt &value,
272  const trace_optionst &options)
273 {
274  irep_idt identifier;
275 
276  if(lhs_object.has_value())
277  identifier=lhs_object->get_identifier();
278 
279  out << from_expr(ns, identifier, full_lhs) << '=';
280 
281  if(value.is_nil())
282  out << "(assignment removed)";
283  else
284  {
285  out << from_expr(ns, identifier, value);
286 
287  // the binary representation
288  out << ' ' << messaget::faint << '('
289  << trace_numeric_value(value, ns, options) << ')' << messaget::reset;
290  }
291 
292  out << '\n';
293 }
294 
295 static std::string
297 {
298  std::string result;
299 
300  const auto &source_location = state.pc->source_location;
301 
302  if(!source_location.get_file().empty())
303  result += "file " + id2string(source_location.get_file());
304 
305  if(!state.function_id.empty())
306  {
307  const symbolt &symbol = ns.lookup(state.function_id);
308  if(!result.empty())
309  result += ' ';
310  result += "function " + id2string(symbol.display_name());
311  }
312 
313  if(!source_location.get_line().empty())
314  {
315  if(!result.empty())
316  result += ' ';
317  result += "line " + id2string(source_location.get_line());
318  }
319 
320  if(!result.empty())
321  result += ' ';
322  result += "thread " + std::to_string(state.thread_nr);
323 
324  return result;
325 }
326 
328  messaget::mstreamt &out,
329  const namespacet &ns,
330  const goto_trace_stept &state,
331  unsigned step_nr,
332  const trace_optionst &options)
333 {
334  out << '\n';
335 
336  if(step_nr == 0)
337  out << "Initial State";
338  else
339  out << "State " << step_nr;
340 
341  out << ' ' << state_location(state, ns) << '\n';
342  out << "----------------------------------------------------" << '\n';
343 
344  if(options.show_code)
345  {
346  out << as_string(ns, state.function_id, *state.pc) << '\n';
347  out << "----------------------------------------------------" << '\n';
348  }
349 }
350 
352 {
353  if(src.id()==ID_index)
354  return is_index_member_symbol(src.op0());
355  else if(src.id()==ID_member)
356  return is_index_member_symbol(src.op0());
357  else if(src.id()==ID_symbol)
358  return true;
359  else
360  return false;
361 }
362 
369  messaget::mstreamt &out,
370  const namespacet &ns,
371  const goto_tracet &goto_trace,
372  const trace_optionst &options)
373 {
374  std::size_t function_depth = 0;
375 
376  for(const auto &step : goto_trace.steps)
377  {
378  if(step.is_function_call())
379  function_depth++;
380  else if(step.is_function_return())
381  function_depth--;
382 
383  // hide the hidden ones
384  if(step.hidden)
385  continue;
386 
387  switch(step.type)
388  {
390  if(!step.cond_value)
391  {
392  out << '\n';
393  out << messaget::red << "Violated property:" << messaget::reset << '\n';
394  if(!step.pc->source_location.is_nil())
395  out << " " << state_location(step, ns) << '\n';
396 
397  out << " " << messaget::red << step.comment << messaget::reset << '\n';
398 
399  if(step.pc->is_assert())
400  {
401  out << " "
402  << from_expr(ns, step.function_id, step.pc->get_condition())
403  << '\n';
404  }
405 
406  out << '\n';
407  }
408  break;
409 
411  if(
412  step.assignment_type ==
414  {
415  break;
416  }
417 
418  out << " ";
419 
420  if(!step.pc->source_location.get_line().empty())
421  {
422  out << messaget::faint << step.pc->source_location.get_line() << ':'
423  << messaget::reset << ' ';
424  }
425 
426  trace_value(
427  out,
428  ns,
429  step.get_lhs_object(),
430  step.full_lhs,
431  step.full_lhs_value,
432  options);
433  break;
434 
436  // downwards arrow
437  out << '\n' << messaget::faint << u8"\u21b3" << messaget::reset << ' ';
438  if(!step.pc->source_location.get_file().empty())
439  {
440  out << messaget::faint << step.pc->source_location.get_file();
441 
442  if(!step.pc->source_location.get_line().empty())
443  {
444  out << messaget::faint << ':' << step.pc->source_location.get_line();
445  }
446 
447  out << messaget::reset << ' ';
448  }
449 
450  {
451  // show the display name
452  const auto &f_symbol = ns.lookup(step.called_function);
453  out << f_symbol.display_name();
454  }
455 
456  {
457  auto arg_strings = make_range(step.function_arguments)
458  .map([&ns, &step](const exprt &arg) {
459  return from_expr(ns, step.function_id, arg);
460  });
461 
462  out << '(';
463  join_strings(out, arg_strings.begin(), arg_strings.end(), ", ");
464  out << ")\n";
465  }
466 
467  break;
468 
470  // upwards arrow
471  out << messaget::faint << u8"\u21b5" << messaget::reset << '\n';
472  break;
473 
488  break;
489 
491  UNREACHABLE;
492  }
493  }
494 }
495 
497  messaget::mstreamt &out,
498  const namespacet &ns,
499  const goto_tracet &goto_trace,
500  const trace_optionst &options)
501 {
502  unsigned prev_step_nr=0;
503  bool first_step=true;
504  std::size_t function_depth=0;
505 
506  for(const auto &step : goto_trace.steps)
507  {
508  // hide the hidden ones
509  if(step.hidden)
510  continue;
511 
512  switch(step.type)
513  {
515  if(!step.cond_value)
516  {
517  out << '\n';
518  out << messaget::red << "Violated property:" << messaget::reset << '\n';
519  if(!step.pc->source_location.is_nil())
520  {
521  out << " " << state_location(step, ns) << '\n';
522  }
523 
524  out << " " << messaget::red << step.comment << messaget::reset << '\n';
525 
526  if(step.pc->is_assert())
527  {
528  out << " "
529  << from_expr(ns, step.function_id, step.pc->get_condition())
530  << '\n';
531  }
532 
533  out << '\n';
534  }
535  break;
536 
538  if(step.cond_value && step.pc->is_assume())
539  {
540  out << "\n";
541  out << "Assumption:\n";
542 
543  if(!step.pc->source_location.is_nil())
544  out << " " << step.pc->source_location << '\n';
545 
546  out << " " << from_expr(ns, step.function_id, step.pc->get_condition())
547  << '\n';
548  }
549  break;
550 
552  break;
553 
555  break;
556 
558  if(step.pc->is_assign() ||
559  step.pc->is_return() || // returns have a lhs!
560  step.pc->is_function_call() ||
561  (step.pc->is_other() && step.full_lhs.is_not_nil()))
562  {
563  if(prev_step_nr!=step.step_nr || first_step)
564  {
565  first_step=false;
566  prev_step_nr=step.step_nr;
567  show_state_header(out, ns, step, step.step_nr, options);
568  }
569 
570  out << " ";
571  trace_value(
572  out,
573  ns,
574  step.get_lhs_object(),
575  step.full_lhs,
576  step.full_lhs_value,
577  options);
578  }
579  break;
580 
582  if(prev_step_nr!=step.step_nr || first_step)
583  {
584  first_step=false;
585  prev_step_nr=step.step_nr;
586  show_state_header(out, ns, step, step.step_nr, options);
587  }
588 
589  out << " ";
590  trace_value(
591  out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
592  break;
593 
595  if(step.formatted)
596  {
597  printf_formattert printf_formatter(ns);
598  printf_formatter(id2string(step.format_string), step.io_args);
599  printf_formatter.print(out);
600  out << '\n';
601  }
602  else
603  {
604  show_state_header(out, ns, step, step.step_nr, options);
605  out << " OUTPUT " << step.io_id << ':';
606 
607  for(std::list<exprt>::const_iterator
608  l_it=step.io_args.begin();
609  l_it!=step.io_args.end();
610  l_it++)
611  {
612  if(l_it!=step.io_args.begin())
613  out << ';';
614 
615  out << ' ' << from_expr(ns, step.function_id, *l_it);
616 
617  // the binary representation
618  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
619  }
620 
621  out << '\n';
622  }
623  break;
624 
626  show_state_header(out, ns, step, step.step_nr, options);
627  out << " INPUT " << step.io_id << ':';
628 
629  for(std::list<exprt>::const_iterator
630  l_it=step.io_args.begin();
631  l_it!=step.io_args.end();
632  l_it++)
633  {
634  if(l_it!=step.io_args.begin())
635  out << ';';
636 
637  out << ' ' << from_expr(ns, step.function_id, *l_it);
638 
639  // the binary representation
640  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
641  }
642 
643  out << '\n';
644  break;
645 
647  function_depth++;
648  if(options.show_function_calls)
649  {
650  out << "\n#### Function call: " << step.called_function;
651  out << '(';
652 
653  bool first = true;
654  for(auto &arg : step.function_arguments)
655  {
656  if(first)
657  first = false;
658  else
659  out << ", ";
660 
661  out << from_expr(ns, step.function_id, arg);
662  }
663 
664  out << ") (depth " << function_depth << ") ####\n";
665  }
666  break;
667 
669  function_depth--;
670  if(options.show_function_calls)
671  {
672  out << "\n#### Function return from " << step.function_id << " (depth "
673  << function_depth << ") ####\n";
674  }
675  break;
676 
682  break;
683 
688  UNREACHABLE;
689  }
690  }
691 }
692 
694  messaget::mstreamt &out,
695  const namespacet &ns,
696  const goto_tracet &goto_trace)
697 {
698  // map from thread number to a call stack
699  std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
700  call_stacks;
701 
702  // by default, we show thread 0
703  unsigned thread_to_show = 0;
704 
705  for(auto s_it = goto_trace.steps.begin(); s_it != goto_trace.steps.end();
706  s_it++)
707  {
708  const auto &step = *s_it;
709  auto &stack = call_stacks[step.thread_nr];
710 
711  if(step.is_assert())
712  {
713  if(!step.cond_value)
714  {
715  stack.push_back(s_it);
716  thread_to_show = step.thread_nr;
717  }
718  }
719  else if(step.is_function_call())
720  {
721  stack.push_back(s_it);
722  }
723  else if(step.is_function_return())
724  {
725  stack.pop_back();
726  }
727  }
728 
729  const auto &stack = call_stacks[thread_to_show];
730 
731  // print in reverse order
732  for(auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
733  {
734  const auto &step = **s_it;
735  if(step.is_assert())
736  {
737  out << " assertion failure";
738  if(!step.pc->source_location.is_nil())
739  out << ' ' << step.pc->source_location;
740  out << '\n';
741  }
742  else if(step.is_function_call())
743  {
744  out << " " << step.called_function;
745  out << '(';
746 
747  bool first = true;
748  for(auto &arg : step.function_arguments)
749  {
750  if(first)
751  first = false;
752  else
753  out << ", ";
754 
755  out << from_expr(ns, step.function_id, arg);
756  }
757 
758  out << ')';
759 
760  if(!step.pc->source_location.is_nil())
761  out << ' ' << step.pc->source_location;
762 
763  out << '\n';
764  }
765  }
766 }
767 
769  messaget::mstreamt &out,
770  const namespacet &ns,
771  const goto_tracet &goto_trace,
772  const trace_optionst &options)
773 {
774  if(options.stack_trace)
775  show_goto_stack_trace(out, ns, goto_trace);
776  else if(options.compact_trace)
777  show_compact_goto_trace(out, ns, goto_trace, options);
778  else
779  show_full_goto_trace(out, ns, goto_trace, options);
780 }
781 
783 
784 std::set<irep_idt> goto_tracet::get_failed_property_ids() const
785 {
786  std::set<irep_idt> property_ids;
787  for(const auto &step : steps)
788  {
789  if(step.is_assert() && !step.cond_value)
790  property_ids.insert(step.property_id);
791  }
792  return property_ids;
793 }
The type of an expression, extends irept.
Definition: type.h:28
BigInt mp_integer
Definition: mp_arith.h:19
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:768
bool is_nil() const
Definition: irep.h:398
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:97
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
const exprt & op() const
Definition: std_expr.h:282
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:191
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:327
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const irep_idt & get_value() const
Definition: std_expr.h:4067
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:81
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:4058
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:329
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:54
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:784
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:62
bool is_function_call() const
Definition: goto_trace.h:60
const irep_idt & id() const
Definition: irep.h:418
bool is_index_member_symbol(const exprt &src)
Definition: goto_trace.cpp:351
Expression classes for byte-level operators.
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:296
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:244
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:125
unsigned thread_nr
Definition: goto_trace.h:115
static const commandt red
render text with red foreground color
Definition: message.h:332
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:464
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:3637
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:49
#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:184
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:4092
std::size_t get_width() const
Definition: std_types.h:1041
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:721
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:371
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:266
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:368
void show_full_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Definition: goto_trace.cpp:496
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:145
Base class for all expressions.
Definition: expr.h:52
const exprt & struct_op() const
Definition: std_expr.h:3583
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:504
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2175
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:693
Trace of a GOTO program.
Definition: goto_trace.h:170
static optionalt< symbol_exprt > get_object_rec(const exprt &src)
Definition: goto_trace.cpp:29
static const trace_optionst default_options
Definition: goto_trace.h:232
const typet & subtype() const
Definition: type.h:47
operandst & operands()
Definition: expr.h:91
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bool empty() const
Definition: dstring.h:88
exprt & array()
Definition: std_expr.h:1397
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1435
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