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/c_types.h>
21 #include <util/format_expr.h>
22 #include <util/merge_irep.h>
23 #include <util/range.h>
24 #include <util/string_utils.h>
25 #include <util/symbol.h>
26 
27 #include <langapi/language_util.h>
28 
29 #include "printf_formatter.h"
30 
32 {
33  if(src.id()==ID_symbol)
34  return to_symbol_expr(src);
35  else if(src.id()==ID_member)
36  return get_object_rec(to_member_expr(src).struct_op());
37  else if(src.id()==ID_index)
38  return get_object_rec(to_index_expr(src).array());
39  else if(src.id()==ID_typecast)
40  return get_object_rec(to_typecast_expr(src).op());
41  else if(
42  src.id() == ID_byte_extract_little_endian ||
43  src.id() == ID_byte_extract_big_endian)
44  {
45  return get_object_rec(to_byte_extract_expr(src).op());
46  }
47  else
48  return {}; // give up
49 }
50 
52 {
53  return get_object_rec(full_lhs);
54 }
55 
57  const class namespacet &ns,
58  std::ostream &out) const
59 {
60  for(const auto &step : steps)
61  step.output(ns, out);
62 }
63 
65  const namespacet &,
66  std::ostream &out) const
67 {
68  out << "*** ";
69 
70  // clang-format off
71  switch(type)
72  {
73  case goto_trace_stept::typet::ASSERT: out << "ASSERT"; break;
74  case goto_trace_stept::typet::ASSUME: out << "ASSUME"; break;
75  case goto_trace_stept::typet::LOCATION: out << "LOCATION"; break;
76  case goto_trace_stept::typet::ASSIGNMENT: out << "ASSIGNMENT"; break;
77  case goto_trace_stept::typet::GOTO: out << "GOTO"; break;
78  case goto_trace_stept::typet::DECL: out << "DECL"; break;
79  case goto_trace_stept::typet::DEAD: out << "DEAD"; break;
80  case goto_trace_stept::typet::OUTPUT: out << "OUTPUT"; break;
81  case goto_trace_stept::typet::INPUT: out << "INPUT"; break;
83  out << "ATOMIC_BEGIN";
84  break;
85  case goto_trace_stept::typet::ATOMIC_END: out << "ATOMIC_END"; break;
86  case goto_trace_stept::typet::SHARED_READ: out << "SHARED_READ"; break;
87  case goto_trace_stept::typet::SHARED_WRITE: out << "SHARED WRITE"; break;
88  case goto_trace_stept::typet::FUNCTION_CALL: out << "FUNCTION CALL"; break;
90  out << "FUNCTION RETURN"; break;
91  case goto_trace_stept::typet::MEMORY_BARRIER: out << "MEMORY_BARRIER"; break;
92  case goto_trace_stept::typet::SPAWN: out << "SPAWN"; break;
93  case goto_trace_stept::typet::CONSTRAINT: out << "CONSTRAINT"; break;
94  case goto_trace_stept::typet::NONE: out << "NONE"; break;
95  }
96  // clang-format on
97 
98  if(is_assert() || is_assume() || is_goto())
99  out << " (" << cond_value << ')';
100  else if(is_function_call())
101  out << ' ' << called_function;
102 
103  if(hidden)
104  out << " hidden";
105 
106  out << '\n';
107 
108  if(is_assignment())
109  {
110  out << " " << format(full_lhs)
111  << " = " << format(full_lhs_value)
112  << '\n';
113  }
114 
115  if(!pc->source_location().is_nil())
116  out << pc->source_location() << '\n';
117 
118  out << pc->type() << '\n';
119 
120  if(pc->is_assert())
121  {
122  if(!cond_value)
123  {
124  out << "Violated property:" << '\n';
125  if(pc->source_location().is_nil())
126  out << " " << pc->source_location() << '\n';
127 
128  if(!comment.empty())
129  out << " " << comment << '\n';
130 
131  out << " " << format(pc->get_condition()) << '\n';
132  out << '\n';
133  }
134  }
135 
136  out << '\n';
137 }
138 
140 {
141  dest(cond_expr);
142  dest(full_lhs);
143  dest(full_lhs_value);
144 
145  for(auto &io_arg : io_args)
146  dest(io_arg);
147 
148  for(auto &function_arg : function_arguments)
149  dest(function_arg);
150 }
151 
161 static std::string numeric_representation(
162  const constant_exprt &expr,
163  const namespacet &ns,
164  const trace_optionst &options)
165 {
166  std::string result;
167  std::string prefix;
168 
169  const typet &expr_type = expr.type();
170 
171  const typet &underlying_type =
172  expr_type.id() == ID_c_enum_tag
173  ? ns.follow_tag(to_c_enum_tag_type(expr_type)).underlying_type()
174  : expr_type;
175 
176  const irep_idt &value = expr.get_value();
177 
178  const auto width = to_bitvector_type(underlying_type).get_width();
179 
180  const mp_integer value_int = bvrep2integer(id2string(value), width, false);
181 
182  if(options.hex_representation)
183  {
184  result = integer2string(value_int, 16);
185  prefix = "0x";
186  }
187  else
188  {
189  result = integer2binary(value_int, width);
190  prefix = "0b";
191  }
192 
193  std::ostringstream oss;
195  for(const auto c : result)
196  {
197  oss << c;
198  if(++i % 8 == 0 && result.size() != i)
199  oss << ' ';
200  }
201  if(options.base_prefix)
202  return prefix + oss.str();
203  else
204  return oss.str();
205 }
206 
208  const exprt &expr,
209  const namespacet &ns,
210  const trace_optionst &options)
211 {
212  const typet &type = expr.type();
213 
214  if(expr.id()==ID_constant)
215  {
216  if(type.id()==ID_unsignedbv ||
217  type.id()==ID_signedbv ||
218  type.id()==ID_bv ||
219  type.id()==ID_fixedbv ||
220  type.id()==ID_floatbv ||
221  type.id()==ID_pointer ||
222  type.id()==ID_c_bit_field ||
223  type.id()==ID_c_bool ||
224  type.id()==ID_c_enum ||
225  type.id()==ID_c_enum_tag)
226  {
227  return numeric_representation(to_constant_expr(expr), ns, options);
228  }
229  else if(type.id()==ID_bool)
230  {
231  return expr.is_true()?"1":"0";
232  }
233  else if(type.id()==ID_integer)
234  {
235  const auto i = numeric_cast<mp_integer>(expr);
236  if(i.has_value() && *i >= 0)
237  {
238  if(options.hex_representation)
239  return "0x" + integer2string(*i, 16);
240  else
241  return "0b" + integer2string(*i, 2);
242  }
243  }
244  }
245  else if(expr.id()==ID_array)
246  {
247  std::string result;
248 
249  forall_operands(it, expr)
250  {
251  if(result.empty())
252  result="{ ";
253  else
254  result+=", ";
255  result+=trace_numeric_value(*it, ns, options);
256  }
257 
258  return result+" }";
259  }
260  else if(expr.id()==ID_struct)
261  {
262  std::string result="{ ";
263 
264  forall_operands(it, expr)
265  {
266  if(it!=expr.operands().begin())
267  result+=", ";
268  result+=trace_numeric_value(*it, ns, options);
269  }
270 
271  return result+" }";
272  }
273  else if(expr.id()==ID_union)
274  {
275  return trace_numeric_value(to_union_expr(expr).op(), ns, options);
276  }
277 
278  return "?";
279 }
280 
281 static void trace_value(
282  messaget::mstreamt &out,
283  const namespacet &ns,
284  const optionalt<symbol_exprt> &lhs_object,
285  const exprt &full_lhs,
286  const exprt &value,
287  const trace_optionst &options)
288 {
289  irep_idt identifier;
290 
291  if(lhs_object.has_value())
292  identifier=lhs_object->get_identifier();
293 
294  out << from_expr(ns, identifier, full_lhs) << '=';
295 
296  if(value.is_nil())
297  out << "(assignment removed)";
298  else
299  {
300  out << from_expr(ns, identifier, value);
301 
302  // the binary representation
303  out << ' ' << messaget::faint << '('
304  << trace_numeric_value(value, ns, options) << ')' << messaget::reset;
305  }
306 
307  out << '\n';
308 }
309 
310 static std::string
312 {
313  std::string result;
314 
315  const auto &source_location = state.pc->source_location();
316 
317  if(!source_location.get_file().empty())
318  result += "file " + id2string(source_location.get_file());
319 
320  if(!state.function_id.empty())
321  {
322  const symbolt &symbol = ns.lookup(state.function_id);
323  if(!result.empty())
324  result += ' ';
325  result += "function " + id2string(symbol.display_name());
326  }
327 
328  if(!source_location.get_line().empty())
329  {
330  if(!result.empty())
331  result += ' ';
332  result += "line " + id2string(source_location.get_line());
333  }
334 
335  if(!result.empty())
336  result += ' ';
337  result += "thread " + std::to_string(state.thread_nr);
338 
339  return result;
340 }
341 
343  messaget::mstreamt &out,
344  const namespacet &ns,
345  const goto_trace_stept &state,
346  unsigned step_nr,
347  const trace_optionst &options)
348 {
349  out << '\n';
350 
351  if(step_nr == 0)
352  out << "Initial State";
353  else
354  out << "State " << step_nr;
355 
356  out << ' ' << state_location(state, ns) << '\n';
357  out << "----------------------------------------------------" << '\n';
358 
359  if(options.show_code)
360  {
361  out << as_string(ns, state.function_id, *state.pc) << '\n';
362  out << "----------------------------------------------------" << '\n';
363  }
364 }
365 
367 {
368  if(src.id()==ID_index)
369  return is_index_member_symbol(to_index_expr(src).array());
370  else if(src.id()==ID_member)
371  return is_index_member_symbol(to_member_expr(src).compound());
372  else if(src.id()==ID_symbol)
373  return true;
374  else
375  return false;
376 }
377 
384  messaget::mstreamt &out,
385  const namespacet &ns,
386  const goto_tracet &goto_trace,
387  const trace_optionst &options)
388 {
389  std::size_t function_depth = 0;
390 
391  for(const auto &step : goto_trace.steps)
392  {
393  if(step.is_function_call())
394  function_depth++;
395  else if(step.is_function_return())
396  function_depth--;
397 
398  // hide the hidden ones
399  if(step.hidden)
400  continue;
401 
402  switch(step.type)
403  {
405  if(!step.cond_value)
406  {
407  out << '\n';
408  out << messaget::red << "Violated property:" << messaget::reset << '\n';
409  if(!step.pc->source_location().is_nil())
410  out << " " << state_location(step, ns) << '\n';
411 
412  out << " " << messaget::red << step.comment << messaget::reset << '\n';
413 
414  if(step.pc->is_assert())
415  {
416  out << " "
417  << from_expr(ns, step.function_id, step.pc->get_condition())
418  << '\n';
419  }
420 
421  out << '\n';
422  }
423  break;
424 
426  if(
427  step.assignment_type ==
429  {
430  break;
431  }
432 
433  out << " ";
434 
435  if(!step.pc->source_location().get_line().empty())
436  {
437  out << messaget::faint << step.pc->source_location().get_line() << ':'
438  << messaget::reset << ' ';
439  }
440 
441  trace_value(
442  out,
443  ns,
444  step.get_lhs_object(),
445  step.full_lhs,
446  step.full_lhs_value,
447  options);
448  break;
449 
451  // downwards arrow
452  out << '\n' << messaget::faint << u8"\u21b3" << messaget::reset << ' ';
453  if(!step.pc->source_location().get_file().empty())
454  {
455  out << messaget::faint << step.pc->source_location().get_file();
456 
457  if(!step.pc->source_location().get_line().empty())
458  {
459  out << messaget::faint << ':'
460  << step.pc->source_location().get_line();
461  }
462 
463  out << messaget::reset << ' ';
464  }
465 
466  {
467  // show the display name
468  const auto &f_symbol = ns.lookup(step.called_function);
469  out << f_symbol.display_name();
470  }
471 
472  {
473  auto arg_strings = make_range(step.function_arguments)
474  .map([&ns, &step](const exprt &arg) {
475  return from_expr(ns, step.function_id, arg);
476  });
477 
478  out << '(';
479  join_strings(out, arg_strings.begin(), arg_strings.end(), ", ");
480  out << ")\n";
481  }
482 
483  break;
484 
486  // upwards arrow
487  out << messaget::faint << u8"\u21b5" << messaget::reset << '\n';
488  break;
489 
504  break;
505 
507  UNREACHABLE;
508  }
509  }
510 }
511 
513  messaget::mstreamt &out,
514  const namespacet &ns,
515  const goto_tracet &goto_trace,
516  const trace_optionst &options)
517 {
518  unsigned prev_step_nr=0;
519  bool first_step=true;
520  std::size_t function_depth=0;
521 
522  for(const auto &step : goto_trace.steps)
523  {
524  // hide the hidden ones
525  if(step.hidden)
526  continue;
527 
528  switch(step.type)
529  {
531  if(!step.cond_value)
532  {
533  out << '\n';
534  out << messaget::red << "Violated property:" << messaget::reset << '\n';
535  if(!step.pc->source_location().is_nil())
536  {
537  out << " " << state_location(step, ns) << '\n';
538  }
539 
540  out << " " << messaget::red << step.comment << messaget::reset << '\n';
541 
542  if(step.pc->is_assert())
543  {
544  out << " "
545  << from_expr(ns, step.function_id, step.pc->get_condition())
546  << '\n';
547  }
548 
549  out << '\n';
550  }
551  break;
552 
554  if(step.cond_value && step.pc->is_assume())
555  {
556  out << "\n";
557  out << "Assumption:\n";
558 
559  if(!step.pc->source_location().is_nil())
560  out << " " << step.pc->source_location() << '\n';
561 
562  out << " " << from_expr(ns, step.function_id, step.pc->get_condition())
563  << '\n';
564  }
565  break;
566 
568  break;
569 
571  break;
572 
574  if(
575  step.pc->is_assign() ||
576  step.pc->is_set_return_value() || // returns have a lhs!
577  step.pc->is_function_call() ||
578  (step.pc->is_other() && step.full_lhs.is_not_nil()))
579  {
580  if(prev_step_nr!=step.step_nr || first_step)
581  {
582  first_step=false;
583  prev_step_nr=step.step_nr;
584  show_state_header(out, ns, step, step.step_nr, options);
585  }
586 
587  out << " ";
588  trace_value(
589  out,
590  ns,
591  step.get_lhs_object(),
592  step.full_lhs,
593  step.full_lhs_value,
594  options);
595  }
596  break;
597 
599  if(prev_step_nr!=step.step_nr || first_step)
600  {
601  first_step=false;
602  prev_step_nr=step.step_nr;
603  show_state_header(out, ns, step, step.step_nr, options);
604  }
605 
606  out << " ";
607  trace_value(
608  out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
609  break;
610 
612  if(step.formatted)
613  {
614  printf_formattert printf_formatter(ns);
615  printf_formatter(id2string(step.format_string), step.io_args);
616  printf_formatter.print(out);
617  out << '\n';
618  }
619  else
620  {
621  show_state_header(out, ns, step, step.step_nr, options);
622  out << " OUTPUT " << step.io_id << ':';
623 
624  for(std::list<exprt>::const_iterator
625  l_it=step.io_args.begin();
626  l_it!=step.io_args.end();
627  l_it++)
628  {
629  if(l_it!=step.io_args.begin())
630  out << ';';
631 
632  out << ' ' << from_expr(ns, step.function_id, *l_it);
633 
634  // the binary representation
635  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
636  }
637 
638  out << '\n';
639  }
640  break;
641 
643  show_state_header(out, ns, step, step.step_nr, options);
644  out << " INPUT " << step.io_id << ':';
645 
646  for(std::list<exprt>::const_iterator
647  l_it=step.io_args.begin();
648  l_it!=step.io_args.end();
649  l_it++)
650  {
651  if(l_it!=step.io_args.begin())
652  out << ';';
653 
654  out << ' ' << from_expr(ns, step.function_id, *l_it);
655 
656  // the binary representation
657  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
658  }
659 
660  out << '\n';
661  break;
662 
664  function_depth++;
665  if(options.show_function_calls)
666  {
667  out << "\n#### Function call: " << step.called_function;
668  out << '(';
669 
670  bool first = true;
671  for(auto &arg : step.function_arguments)
672  {
673  if(first)
674  first = false;
675  else
676  out << ", ";
677 
678  out << from_expr(ns, step.function_id, arg);
679  }
680 
681  out << ") (depth " << function_depth << ") ####\n";
682  }
683  break;
684 
686  function_depth--;
687  if(options.show_function_calls)
688  {
689  out << "\n#### Function return from " << step.function_id << " (depth "
690  << function_depth << ") ####\n";
691  }
692  break;
693 
699  break;
700 
705  UNREACHABLE;
706  }
707  }
708 }
709 
711  messaget::mstreamt &out,
712  const namespacet &ns,
713  const goto_tracet &goto_trace)
714 {
715  // map from thread number to a call stack
716  std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
717  call_stacks;
718 
719  // by default, we show thread 0
720  unsigned thread_to_show = 0;
721 
722  for(auto s_it = goto_trace.steps.begin(); s_it != goto_trace.steps.end();
723  s_it++)
724  {
725  const auto &step = *s_it;
726  auto &stack = call_stacks[step.thread_nr];
727 
728  if(step.is_assert())
729  {
730  if(!step.cond_value)
731  {
732  stack.push_back(s_it);
733  thread_to_show = step.thread_nr;
734  }
735  }
736  else if(step.is_function_call())
737  {
738  stack.push_back(s_it);
739  }
740  else if(step.is_function_return())
741  {
742  stack.pop_back();
743  }
744  }
745 
746  const auto &stack = call_stacks[thread_to_show];
747 
748  // print in reverse order
749  for(auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
750  {
751  const auto &step = **s_it;
752  if(step.is_assert())
753  {
754  out << " assertion failure";
755  if(!step.pc->source_location().is_nil())
756  out << ' ' << step.pc->source_location();
757  out << '\n';
758  }
759  else if(step.is_function_call())
760  {
761  out << " " << step.called_function;
762  out << '(';
763 
764  bool first = true;
765  for(auto &arg : step.function_arguments)
766  {
767  if(first)
768  first = false;
769  else
770  out << ", ";
771 
772  out << from_expr(ns, step.function_id, arg);
773  }
774 
775  out << ')';
776 
777  if(!step.pc->source_location().is_nil())
778  out << ' ' << step.pc->source_location();
779 
780  out << '\n';
781  }
782  }
783 }
784 
786  messaget::mstreamt &out,
787  const namespacet &ns,
788  const goto_tracet &goto_trace,
789  const trace_optionst &options)
790 {
791  if(options.stack_trace)
792  show_goto_stack_trace(out, ns, goto_trace);
793  else if(options.compact_trace)
794  show_compact_goto_trace(out, ns, goto_trace, options);
795  else
796  show_full_goto_trace(out, ns, goto_trace, options);
797 }
798 
800 
801 std::set<irep_idt> goto_tracet::get_failed_property_ids() const
802 {
803  std::set<irep_idt> property_ids;
804  for(const auto &step : steps)
805  {
806  if(step.is_assert() && !step.cond_value)
807  property_ids.insert(step.property_id);
808  }
809  return property_ids;
810 }
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
uint64_t u8
Definition: bytecode_info.h:58
unsignedbv_typet size_type()
Definition: c_types.cpp:68
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:344
std::size_t get_width() const
Definition: std_types.h:864
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
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
Base class for all expressions.
Definition: expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
std::vector< exprt > function_arguments
Definition: goto_trace.h:144
bool is_function_call() const
Definition: goto_trace.h:60
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:51
bool is_assignment() const
Definition: goto_trace.h:55
std::string comment
Definition: goto_trace.h:123
exprt full_lhs_value
Definition: goto_trace.h:132
goto_programt::const_targett pc
Definition: goto_trace.h:112
irep_idt function_id
Definition: goto_trace.h:111
io_argst io_args
Definition: goto_trace.h:137
void merge_ireps(merge_irept &dest)
Use dest to establish sharing among ireps.
Definition: goto_trace.cpp:139
unsigned thread_nr
Definition: goto_trace.h:115
bool is_goto() const
Definition: goto_trace.h:58
bool is_assume() const
Definition: goto_trace.h:56
bool is_assert() const
Definition: goto_trace.h:57
irep_idt called_function
Definition: goto_trace.h:141
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace step in ASCII to a given stream.
Definition: goto_trace.cpp:64
Trace of a GOTO program.
Definition: goto_trace.h:175
stepst steps
Definition: goto_trace.h:178
std::set< irep_idt > get_failed_property_ids() const
Returns the property IDs of all failed assertions in the trace.
Definition: goto_trace.cpp:801
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace in ASCII to a given stream.
Definition: goto_trace.cpp:56
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
source_locationt source_location
Definition: message.h:247
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:343
static const commandt faint
render text with faint font
Definition: message.h:385
static const commandt red
render text with red foreground color
Definition: message.h:346
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
void print(std::ostream &out)
Symbol table entry.
Definition: symbol.h:28
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
The type of an expression, extends irept.
Definition: type.h:29
#define forall_operands(it, expr)
Definition: expr.h:18
static format_containert< T > format(const T &o)
Definition: format.h:37
static void show_goto_stack_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:710
static std::string state_location(const goto_trace_stept &state, const namespacet &ns)
Definition: goto_trace.cpp:311
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:342
std::string trace_numeric_value(const exprt &expr, const namespacet &ns, const trace_optionst &options)
Definition: goto_trace.cpp:207
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:161
void show_full_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Definition: goto_trace.cpp:512
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:785
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:281
bool is_index_member_symbol(const exprt &src)
Definition: goto_trace.cpp:366
static optionalt< symbol_exprt > get_object_rec(const exprt &src)
Definition: goto_trace.cpp:31
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:383
Traces of GOTO Programs.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:64
nonstd::optional< T > optionalt
Definition: optional.h:35
printf Formatting
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1657
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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:62
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:219
static const trace_optionst default_options
Definition: goto_trace.h:236
bool hex_representation
Represent plain trace values in hex.
Definition: goto_trace.h:223
bool base_prefix
Use prefix (0b or 0x) for distinguishing the base of the representation.
Definition: goto_trace.h:226
bool show_code
Show original code in plain text trace.
Definition: goto_trace.h:230
bool compact_trace
Give a compact trace.
Definition: goto_trace.h:232
bool show_function_calls
Show function calls in plain text trace.
Definition: goto_trace.h:228
bool stack_trace
Give a stack trace only.
Definition: goto_trace.h:234
Symbol table entry.