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)).subtype()
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 << ':' << step.pc->source_location.get_line();
460  }
461 
462  out << messaget::reset << ' ';
463  }
464 
465  {
466  // show the display name
467  const auto &f_symbol = ns.lookup(step.called_function);
468  out << f_symbol.display_name();
469  }
470 
471  {
472  auto arg_strings = make_range(step.function_arguments)
473  .map([&ns, &step](const exprt &arg) {
474  return from_expr(ns, step.function_id, arg);
475  });
476 
477  out << '(';
478  join_strings(out, arg_strings.begin(), arg_strings.end(), ", ");
479  out << ")\n";
480  }
481 
482  break;
483 
485  // upwards arrow
486  out << messaget::faint << u8"\u21b5" << messaget::reset << '\n';
487  break;
488 
503  break;
504 
506  UNREACHABLE;
507  }
508  }
509 }
510 
512  messaget::mstreamt &out,
513  const namespacet &ns,
514  const goto_tracet &goto_trace,
515  const trace_optionst &options)
516 {
517  unsigned prev_step_nr=0;
518  bool first_step=true;
519  std::size_t function_depth=0;
520 
521  for(const auto &step : goto_trace.steps)
522  {
523  // hide the hidden ones
524  if(step.hidden)
525  continue;
526 
527  switch(step.type)
528  {
530  if(!step.cond_value)
531  {
532  out << '\n';
533  out << messaget::red << "Violated property:" << messaget::reset << '\n';
534  if(!step.pc->source_location.is_nil())
535  {
536  out << " " << state_location(step, ns) << '\n';
537  }
538 
539  out << " " << messaget::red << step.comment << messaget::reset << '\n';
540 
541  if(step.pc->is_assert())
542  {
543  out << " "
544  << from_expr(ns, step.function_id, step.pc->get_condition())
545  << '\n';
546  }
547 
548  out << '\n';
549  }
550  break;
551 
553  if(step.cond_value && step.pc->is_assume())
554  {
555  out << "\n";
556  out << "Assumption:\n";
557 
558  if(!step.pc->source_location.is_nil())
559  out << " " << step.pc->source_location << '\n';
560 
561  out << " " << from_expr(ns, step.function_id, step.pc->get_condition())
562  << '\n';
563  }
564  break;
565 
567  break;
568 
570  break;
571 
573  if(
574  step.pc->is_assign() ||
575  step.pc->is_set_return_value() || // returns have a lhs!
576  step.pc->is_function_call() ||
577  (step.pc->is_other() && step.full_lhs.is_not_nil()))
578  {
579  if(prev_step_nr!=step.step_nr || first_step)
580  {
581  first_step=false;
582  prev_step_nr=step.step_nr;
583  show_state_header(out, ns, step, step.step_nr, options);
584  }
585 
586  out << " ";
587  trace_value(
588  out,
589  ns,
590  step.get_lhs_object(),
591  step.full_lhs,
592  step.full_lhs_value,
593  options);
594  }
595  break;
596 
598  if(prev_step_nr!=step.step_nr || first_step)
599  {
600  first_step=false;
601  prev_step_nr=step.step_nr;
602  show_state_header(out, ns, step, step.step_nr, options);
603  }
604 
605  out << " ";
606  trace_value(
607  out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
608  break;
609 
611  if(step.formatted)
612  {
613  printf_formattert printf_formatter(ns);
614  printf_formatter(id2string(step.format_string), step.io_args);
615  printf_formatter.print(out);
616  out << '\n';
617  }
618  else
619  {
620  show_state_header(out, ns, step, step.step_nr, options);
621  out << " OUTPUT " << step.io_id << ':';
622 
623  for(std::list<exprt>::const_iterator
624  l_it=step.io_args.begin();
625  l_it!=step.io_args.end();
626  l_it++)
627  {
628  if(l_it!=step.io_args.begin())
629  out << ';';
630 
631  out << ' ' << from_expr(ns, step.function_id, *l_it);
632 
633  // the binary representation
634  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
635  }
636 
637  out << '\n';
638  }
639  break;
640 
642  show_state_header(out, ns, step, step.step_nr, options);
643  out << " INPUT " << step.io_id << ':';
644 
645  for(std::list<exprt>::const_iterator
646  l_it=step.io_args.begin();
647  l_it!=step.io_args.end();
648  l_it++)
649  {
650  if(l_it!=step.io_args.begin())
651  out << ';';
652 
653  out << ' ' << from_expr(ns, step.function_id, *l_it);
654 
655  // the binary representation
656  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
657  }
658 
659  out << '\n';
660  break;
661 
663  function_depth++;
664  if(options.show_function_calls)
665  {
666  out << "\n#### Function call: " << step.called_function;
667  out << '(';
668 
669  bool first = true;
670  for(auto &arg : step.function_arguments)
671  {
672  if(first)
673  first = false;
674  else
675  out << ", ";
676 
677  out << from_expr(ns, step.function_id, arg);
678  }
679 
680  out << ") (depth " << function_depth << ") ####\n";
681  }
682  break;
683 
685  function_depth--;
686  if(options.show_function_calls)
687  {
688  out << "\n#### Function return from " << step.function_id << " (depth "
689  << function_depth << ") ####\n";
690  }
691  break;
692 
698  break;
699 
704  UNREACHABLE;
705  }
706  }
707 }
708 
710  messaget::mstreamt &out,
711  const namespacet &ns,
712  const goto_tracet &goto_trace)
713 {
714  // map from thread number to a call stack
715  std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
716  call_stacks;
717 
718  // by default, we show thread 0
719  unsigned thread_to_show = 0;
720 
721  for(auto s_it = goto_trace.steps.begin(); s_it != goto_trace.steps.end();
722  s_it++)
723  {
724  const auto &step = *s_it;
725  auto &stack = call_stacks[step.thread_nr];
726 
727  if(step.is_assert())
728  {
729  if(!step.cond_value)
730  {
731  stack.push_back(s_it);
732  thread_to_show = step.thread_nr;
733  }
734  }
735  else if(step.is_function_call())
736  {
737  stack.push_back(s_it);
738  }
739  else if(step.is_function_return())
740  {
741  stack.pop_back();
742  }
743  }
744 
745  const auto &stack = call_stacks[thread_to_show];
746 
747  // print in reverse order
748  for(auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
749  {
750  const auto &step = **s_it;
751  if(step.is_assert())
752  {
753  out << " assertion failure";
754  if(!step.pc->source_location.is_nil())
755  out << ' ' << step.pc->source_location;
756  out << '\n';
757  }
758  else if(step.is_function_call())
759  {
760  out << " " << step.called_function;
761  out << '(';
762 
763  bool first = true;
764  for(auto &arg : step.function_arguments)
765  {
766  if(first)
767  first = false;
768  else
769  out << ", ";
770 
771  out << from_expr(ns, step.function_id, arg);
772  }
773 
774  out << ')';
775 
776  if(!step.pc->source_location.is_nil())
777  out << ' ' << step.pc->source_location;
778 
779  out << '\n';
780  }
781  }
782 }
783 
785  messaget::mstreamt &out,
786  const namespacet &ns,
787  const goto_tracet &goto_trace,
788  const trace_optionst &options)
789 {
790  if(options.stack_trace)
791  show_goto_stack_trace(out, ns, goto_trace);
792  else if(options.compact_trace)
793  show_compact_goto_trace(out, ns, goto_trace, options);
794  else
795  show_full_goto_trace(out, ns, goto_trace, options);
796 }
797 
799 
800 std::set<irep_idt> goto_tracet::get_failed_property_ids() const
801 {
802  std::set<irep_idt> property_ids;
803  for(const auto &step : steps)
804  {
805  if(step.is_assert() && !step.cond_value)
806  property_ids.insert(step.property_id);
807  }
808  return property_ids;
809 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
trace_optionst::compact_trace
bool compact_trace
Give a compact trace.
Definition: goto_trace.h:232
goto_tracet::get_failed_property_ids
std::set< irep_idt > get_failed_property_ids() const
Returns the property IDs of all failed assertions in the trace.
Definition: goto_trace.cpp:800
format
static format_containert< T > format(const T &o)
Definition: format.h:37
goto_trace_stept::typet::LOCATION
@ LOCATION
goto_trace_stept::full_lhs_value
exprt full_lhs_value
Definition: goto_trace.h:132
typet::subtype
const typet & subtype() const
Definition: type.h:47
goto_trace_stept::get_lhs_object
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:51
goto_trace_stept::comment
std::string comment
Definition: goto_trace.h:123
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
show_full_goto_trace
void show_full_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Definition: goto_trace.cpp:511
goto_trace_stept::typet::ASSUME
@ ASSUME
arith_tools.h
printf_formattert
Definition: printf_formatter.h:20
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:343
printf_formatter.h
printf Formatting
merge_irep.h
string_utils.h
trace_optionst::base_prefix
bool base_prefix
Use prefix (0b or 0x) for distinguishing the base of the representation.
Definition: goto_trace.h:226
symbolt::display_name
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
typet
The type of an expression, extends irept.
Definition: type.h:28
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
state_location
static std::string state_location(const goto_trace_stept &state, const namespacet &ns)
Definition: goto_trace.cpp:311
u8
uint64_t u8
Definition: bytecode_info.h:58
trace_optionst::show_code
bool show_code
Show original code in plain text trace.
Definition: goto_trace.h:230
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
goto_trace_stept::is_assert
bool is_assert() const
Definition: goto_trace.h:57
goto_trace_stept::type
typet type
Definition: goto_trace.h:97
goto_tracet::steps
stepst steps
Definition: goto_trace.h:178
exprt
Base class for all expressions.
Definition: expr.h:54
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1648
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
goto_trace_stept
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
goto_trace_stept::is_function_call
bool is_function_call() const
Definition: goto_trace.h:60
goto_trace_stept::called_function
irep_idt called_function
Definition: goto_trace.h:141
goto_trace_stept::is_assignment
bool is_assignment() const
Definition: goto_trace.h:55
goto_trace.h
Traces of GOTO Programs.
printf_formattert::print
void print(std::ostream &out)
Definition: printf_formatter.cpp:38
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
byte_operators.h
Expression classes for byte-level operators.
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
show_compact_goto_trace
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
messaget::faint
static const commandt faint
render text with faint font
Definition: message.h:385
goto_trace_stept::typet::DECL
@ DECL
goto_trace_stept::output
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
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
goto_trace_stept::typet::ASSERT
@ ASSERT
goto_trace_stept::cond_expr
exprt cond_expr
Definition: goto_trace.h:119
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
to_c_enum_tag_type
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:317
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
language_util.h
goto_trace_stept::typet::NONE
@ NONE
join_strings
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
trace_value
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
goto_trace_stept::full_lhs
exprt full_lhs
Definition: goto_trace.h:126
goto_trace_stept::function_arguments
std::vector< exprt > function_arguments
Definition: goto_trace.h:144
goto_trace_stept::pc
goto_programt::const_targett pc
Definition: goto_trace.h:112
is_index_member_symbol
bool is_index_member_symbol(const exprt &src)
Definition: goto_trace.cpp:366
get_object_rec
static optionalt< symbol_exprt > get_object_rec(const exprt &src)
Definition: goto_trace.cpp:31
goto_trace_stept::typet::ASSIGNMENT
@ ASSIGNMENT
goto_tracet::output
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace in ASCII to a given stream.
Definition: goto_trace.cpp:56
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
symbol.h
Symbol table entry.
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
dstringt::empty
bool empty() const
Definition: dstring.h:88
goto_trace_stept::assignment_typet::ACTUAL_PARAMETER
@ ACTUAL_PARAMETER
goto_trace_stept::typet::INPUT
@ INPUT
goto_trace_stept::typet::ATOMIC_END
@ ATOMIC_END
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_trace_stept::thread_nr
unsigned thread_nr
Definition: goto_trace.h:115
goto_trace_stept::typet::SPAWN
@ SPAWN
show_state_header
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
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:843
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
goto_trace_stept::merge_ireps
void merge_ireps(merge_irept &dest)
Use dest to establish sharing among ireps.
Definition: goto_trace.cpp:139
goto_trace_stept::cond_value
bool cond_value
Definition: goto_trace.h:118
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:401
trace_optionst::hex_representation
bool hex_representation
Represent plain trace values in hex.
Definition: goto_trace.h:223
trace_optionst::stack_trace
bool stack_trace
Give a stack trace only.
Definition: goto_trace.h:234
format_expr.h
goto_trace_stept::typet::GOTO
@ GOTO
merge_irept
Definition: merge_irep.h:106
show_goto_trace
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:784
messaget::red
static const commandt red
render text with red foreground color
Definition: message.h:346
trace_optionst
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:219
trace_optionst::show_function_calls
bool show_function_calls
Show function calls in plain text trace.
Definition: goto_trace.h:228
trace_optionst::default_options
static const trace_optionst default_options
Definition: goto_trace.h:236
symbolt
Symbol table entry.
Definition: symbol.h:28
numeric_representation
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
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
goto_trace_stept::hidden
bool hidden
Definition: goto_trace.h:100
trace_numeric_value
std::string trace_numeric_value(const exprt &expr, const namespacet &ns, const trace_optionst &options)
Definition: goto_trace.cpp:207
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:175
show_goto_stack_trace
static void show_goto_stack_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:709
as_string
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:23
messaget::mstreamt
Definition: message.h:224
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
goto_trace_stept::is_assume
bool is_assume() const
Definition: goto_trace.h:56
exprt::operands
operandst & operands()
Definition: expr.h:92
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
goto_trace_stept::is_goto
bool is_goto() const
Definition: goto_trace.h:58
integer2binary
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:64
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
constant_exprt
A constant literal expression.
Definition: std_expr.h:2753
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2761
goto_trace_stept::io_args
io_argst io_args
Definition: goto_trace.h:137
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
goto_trace_stept::function_id
irep_idt function_id
Definition: goto_trace.h:111
c_types.h
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
goto_trace_stept::typet::DEAD
@ DEAD
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103