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