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)
34  return get_object_rec(to_member_expr(src).struct_op());
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  return trace_numeric_value(to_union_expr(expr).op(), ns, options);
260  }
261 
262  return "?";
263 }
264 
265 static void trace_value(
266  messaget::mstreamt &out,
267  const namespacet &ns,
268  const optionalt<symbol_exprt> &lhs_object,
269  const exprt &full_lhs,
270  const exprt &value,
271  const trace_optionst &options)
272 {
273  irep_idt identifier;
274 
275  if(lhs_object.has_value())
276  identifier=lhs_object->get_identifier();
277 
278  out << from_expr(ns, identifier, full_lhs) << '=';
279 
280  if(value.is_nil())
281  out << "(assignment removed)";
282  else
283  {
284  out << from_expr(ns, identifier, value);
285 
286  // the binary representation
287  out << ' ' << messaget::faint << '('
288  << trace_numeric_value(value, ns, options) << ')' << messaget::reset;
289  }
290 
291  out << '\n';
292 }
293 
294 static std::string
296 {
297  std::string result;
298 
299  const auto &source_location = state.pc->source_location;
300 
301  if(!source_location.get_file().empty())
302  result += "file " + id2string(source_location.get_file());
303 
304  if(!state.function_id.empty())
305  {
306  const symbolt &symbol = ns.lookup(state.function_id);
307  if(!result.empty())
308  result += ' ';
309  result += "function " + id2string(symbol.display_name());
310  }
311 
312  if(!source_location.get_line().empty())
313  {
314  if(!result.empty())
315  result += ' ';
316  result += "line " + id2string(source_location.get_line());
317  }
318 
319  if(!result.empty())
320  result += ' ';
321  result += "thread " + std::to_string(state.thread_nr);
322 
323  return result;
324 }
325 
327  messaget::mstreamt &out,
328  const namespacet &ns,
329  const goto_trace_stept &state,
330  unsigned step_nr,
331  const trace_optionst &options)
332 {
333  out << '\n';
334 
335  if(step_nr == 0)
336  out << "Initial State";
337  else
338  out << "State " << step_nr;
339 
340  out << ' ' << state_location(state, ns) << '\n';
341  out << "----------------------------------------------------" << '\n';
342 
343  if(options.show_code)
344  {
345  out << as_string(ns, state.function_id, *state.pc) << '\n';
346  out << "----------------------------------------------------" << '\n';
347  }
348 }
349 
351 {
352  if(src.id()==ID_index)
353  return is_index_member_symbol(to_index_expr(src).array());
354  else if(src.id()==ID_member)
355  return is_index_member_symbol(to_member_expr(src).compound());
356  else if(src.id()==ID_symbol)
357  return true;
358  else
359  return false;
360 }
361 
368  messaget::mstreamt &out,
369  const namespacet &ns,
370  const goto_tracet &goto_trace,
371  const trace_optionst &options)
372 {
373  std::size_t function_depth = 0;
374 
375  for(const auto &step : goto_trace.steps)
376  {
377  if(step.is_function_call())
378  function_depth++;
379  else if(step.is_function_return())
380  function_depth--;
381 
382  // hide the hidden ones
383  if(step.hidden)
384  continue;
385 
386  switch(step.type)
387  {
389  if(!step.cond_value)
390  {
391  out << '\n';
392  out << messaget::red << "Violated property:" << messaget::reset << '\n';
393  if(!step.pc->source_location.is_nil())
394  out << " " << state_location(step, ns) << '\n';
395 
396  out << " " << messaget::red << step.comment << messaget::reset << '\n';
397 
398  if(step.pc->is_assert())
399  {
400  out << " "
401  << from_expr(ns, step.function_id, step.pc->get_condition())
402  << '\n';
403  }
404 
405  out << '\n';
406  }
407  break;
408 
410  if(
411  step.assignment_type ==
413  {
414  break;
415  }
416 
417  out << " ";
418 
419  if(!step.pc->source_location.get_line().empty())
420  {
421  out << messaget::faint << step.pc->source_location.get_line() << ':'
422  << messaget::reset << ' ';
423  }
424 
425  trace_value(
426  out,
427  ns,
428  step.get_lhs_object(),
429  step.full_lhs,
430  step.full_lhs_value,
431  options);
432  break;
433 
435  // downwards arrow
436  out << '\n' << messaget::faint << u8"\u21b3" << messaget::reset << ' ';
437  if(!step.pc->source_location.get_file().empty())
438  {
439  out << messaget::faint << step.pc->source_location.get_file();
440 
441  if(!step.pc->source_location.get_line().empty())
442  {
443  out << messaget::faint << ':' << step.pc->source_location.get_line();
444  }
445 
446  out << messaget::reset << ' ';
447  }
448 
449  {
450  // show the display name
451  const auto &f_symbol = ns.lookup(step.called_function);
452  out << f_symbol.display_name();
453  }
454 
455  {
456  auto arg_strings = make_range(step.function_arguments)
457  .map([&ns, &step](const exprt &arg) {
458  return from_expr(ns, step.function_id, arg);
459  });
460 
461  out << '(';
462  join_strings(out, arg_strings.begin(), arg_strings.end(), ", ");
463  out << ")\n";
464  }
465 
466  break;
467 
469  // upwards arrow
470  out << messaget::faint << u8"\u21b5" << messaget::reset << '\n';
471  break;
472 
487  break;
488 
490  UNREACHABLE;
491  }
492  }
493 }
494 
496  messaget::mstreamt &out,
497  const namespacet &ns,
498  const goto_tracet &goto_trace,
499  const trace_optionst &options)
500 {
501  unsigned prev_step_nr=0;
502  bool first_step=true;
503  std::size_t function_depth=0;
504 
505  for(const auto &step : goto_trace.steps)
506  {
507  // hide the hidden ones
508  if(step.hidden)
509  continue;
510 
511  switch(step.type)
512  {
514  if(!step.cond_value)
515  {
516  out << '\n';
517  out << messaget::red << "Violated property:" << messaget::reset << '\n';
518  if(!step.pc->source_location.is_nil())
519  {
520  out << " " << state_location(step, ns) << '\n';
521  }
522 
523  out << " " << messaget::red << step.comment << messaget::reset << '\n';
524 
525  if(step.pc->is_assert())
526  {
527  out << " "
528  << from_expr(ns, step.function_id, step.pc->get_condition())
529  << '\n';
530  }
531 
532  out << '\n';
533  }
534  break;
535 
537  if(step.cond_value && step.pc->is_assume())
538  {
539  out << "\n";
540  out << "Assumption:\n";
541 
542  if(!step.pc->source_location.is_nil())
543  out << " " << step.pc->source_location << '\n';
544 
545  out << " " << from_expr(ns, step.function_id, step.pc->get_condition())
546  << '\n';
547  }
548  break;
549 
551  break;
552 
554  break;
555 
557  if(step.pc->is_assign() ||
558  step.pc->is_return() || // returns have a lhs!
559  step.pc->is_function_call() ||
560  (step.pc->is_other() && step.full_lhs.is_not_nil()))
561  {
562  if(prev_step_nr!=step.step_nr || first_step)
563  {
564  first_step=false;
565  prev_step_nr=step.step_nr;
566  show_state_header(out, ns, step, step.step_nr, options);
567  }
568 
569  out << " ";
570  trace_value(
571  out,
572  ns,
573  step.get_lhs_object(),
574  step.full_lhs,
575  step.full_lhs_value,
576  options);
577  }
578  break;
579 
581  if(prev_step_nr!=step.step_nr || first_step)
582  {
583  first_step=false;
584  prev_step_nr=step.step_nr;
585  show_state_header(out, ns, step, step.step_nr, options);
586  }
587 
588  out << " ";
589  trace_value(
590  out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
591  break;
592 
594  if(step.formatted)
595  {
596  printf_formattert printf_formatter(ns);
597  printf_formatter(id2string(step.format_string), step.io_args);
598  printf_formatter.print(out);
599  out << '\n';
600  }
601  else
602  {
603  show_state_header(out, ns, step, step.step_nr, options);
604  out << " OUTPUT " << step.io_id << ':';
605 
606  for(std::list<exprt>::const_iterator
607  l_it=step.io_args.begin();
608  l_it!=step.io_args.end();
609  l_it++)
610  {
611  if(l_it!=step.io_args.begin())
612  out << ';';
613 
614  out << ' ' << from_expr(ns, step.function_id, *l_it);
615 
616  // the binary representation
617  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
618  }
619 
620  out << '\n';
621  }
622  break;
623 
625  show_state_header(out, ns, step, step.step_nr, options);
626  out << " INPUT " << step.io_id << ':';
627 
628  for(std::list<exprt>::const_iterator
629  l_it=step.io_args.begin();
630  l_it!=step.io_args.end();
631  l_it++)
632  {
633  if(l_it!=step.io_args.begin())
634  out << ';';
635 
636  out << ' ' << from_expr(ns, step.function_id, *l_it);
637 
638  // the binary representation
639  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
640  }
641 
642  out << '\n';
643  break;
644 
646  function_depth++;
647  if(options.show_function_calls)
648  {
649  out << "\n#### Function call: " << step.called_function;
650  out << '(';
651 
652  bool first = true;
653  for(auto &arg : step.function_arguments)
654  {
655  if(first)
656  first = false;
657  else
658  out << ", ";
659 
660  out << from_expr(ns, step.function_id, arg);
661  }
662 
663  out << ") (depth " << function_depth << ") ####\n";
664  }
665  break;
666 
668  function_depth--;
669  if(options.show_function_calls)
670  {
671  out << "\n#### Function return from " << step.function_id << " (depth "
672  << function_depth << ") ####\n";
673  }
674  break;
675 
681  break;
682 
687  UNREACHABLE;
688  }
689  }
690 }
691 
693  messaget::mstreamt &out,
694  const namespacet &ns,
695  const goto_tracet &goto_trace)
696 {
697  // map from thread number to a call stack
698  std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
699  call_stacks;
700 
701  // by default, we show thread 0
702  unsigned thread_to_show = 0;
703 
704  for(auto s_it = goto_trace.steps.begin(); s_it != goto_trace.steps.end();
705  s_it++)
706  {
707  const auto &step = *s_it;
708  auto &stack = call_stacks[step.thread_nr];
709 
710  if(step.is_assert())
711  {
712  if(!step.cond_value)
713  {
714  stack.push_back(s_it);
715  thread_to_show = step.thread_nr;
716  }
717  }
718  else if(step.is_function_call())
719  {
720  stack.push_back(s_it);
721  }
722  else if(step.is_function_return())
723  {
724  stack.pop_back();
725  }
726  }
727 
728  const auto &stack = call_stacks[thread_to_show];
729 
730  // print in reverse order
731  for(auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
732  {
733  const auto &step = **s_it;
734  if(step.is_assert())
735  {
736  out << " assertion failure";
737  if(!step.pc->source_location.is_nil())
738  out << ' ' << step.pc->source_location;
739  out << '\n';
740  }
741  else if(step.is_function_call())
742  {
743  out << " " << step.called_function;
744  out << '(';
745 
746  bool first = true;
747  for(auto &arg : step.function_arguments)
748  {
749  if(first)
750  first = false;
751  else
752  out << ", ";
753 
754  out << from_expr(ns, step.function_id, arg);
755  }
756 
757  out << ')';
758 
759  if(!step.pc->source_location.is_nil())
760  out << ' ' << step.pc->source_location;
761 
762  out << '\n';
763  }
764  }
765 }
766 
768  messaget::mstreamt &out,
769  const namespacet &ns,
770  const goto_tracet &goto_trace,
771  const trace_optionst &options)
772 {
773  if(options.stack_trace)
774  show_goto_stack_trace(out, ns, goto_trace);
775  else if(options.compact_trace)
776  show_compact_goto_trace(out, ns, goto_trace, options);
777  else
778  show_full_goto_trace(out, ns, goto_trace, options);
779 }
780 
782 
783 std::set<irep_idt> goto_tracet::get_failed_property_ids() const
784 {
785  std::set<irep_idt> property_ids;
786  for(const auto &step : steps)
787  {
788  if(step.is_assert() && !step.cond_value)
789  property_ids.insert(step.property_id);
790  }
791  return property_ids;
792 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
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: std_types.h:721
trace_optionst::compact_trace
bool compact_trace
Give a compact trace.
Definition: goto_trace.h:228
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:783
format
static format_containert< T > format(const T &o)
Definition: format.h:35
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:49
goto_trace_stept::comment
std::string comment
Definition: goto_trace.h:123
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:495
goto_trace_stept::typet::ASSUME
@ ASSUME
arith_tools.h
printf_formattert
Definition: printf_formatter.h:21
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:343
printf_formatter.h
printf Formatting
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:222
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:29
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:295
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:226
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
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:174
exprt
Base class for all expressions.
Definition: expr.h:53
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1613
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
goto_trace_stept
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
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:37
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
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:367
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:62
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_trace_stept::typet::ASSERT
@ ASSERT
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
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:64
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:265
goto_trace_stept::full_lhs
exprt full_lhs
Definition: goto_trace.h:126
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:350
get_object_rec
static optionalt< symbol_exprt > get_object_rec(const exprt &src)
Definition: goto_trace.cpp:29
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:54
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
symbol.h
Symbol table entry.
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:326
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
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:219
trace_optionst::stack_trace
bool stack_trace
Give a stack trace only.
Definition: goto_trace.h:230
format_expr.h
goto_trace_stept::typet::GOTO
@ GOTO
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:767
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:215
trace_optionst::show_function_calls
bool show_function_calls
Show function calls in plain text trace.
Definition: goto_trace.h:224
trace_optionst::default_options
static const trace_optionst default_options
Definition: goto_trace.h:232
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:145
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
as_string
std::string as_string(resultt result)
Definition: properties.cpp:20
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:191
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
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:692
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:3489
goto_trace_stept::is_assume
bool is_assume() const
Definition: goto_trace.h:56
exprt::operands
operandst & operands()
Definition: expr.h:95
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:67
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:3906
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
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
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
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:3939
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106