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/format_expr.h>
20 #include <util/range.h>
21 #include <util/string_utils.h>
22 #include <util/symbol.h>
23 
24 #include <langapi/language_util.h>
25 
26 #include "printf_formatter.h"
27 
29 {
30  if(src.id()==ID_symbol)
31  return to_symbol_expr(src);
32  else if(src.id()==ID_member)
33  return get_object_rec(to_member_expr(src).struct_op());
34  else if(src.id()==ID_index)
35  return get_object_rec(to_index_expr(src).array());
36  else if(src.id()==ID_typecast)
37  return get_object_rec(to_typecast_expr(src).op());
38  else
39  return {}; // give up
40 }
41 
43 {
44  return get_object_rec(full_lhs);
45 }
46 
48  const class namespacet &ns,
49  std::ostream &out) const
50 {
51  for(const auto &step : steps)
52  step.output(ns, out);
53 }
54 
56  const namespacet &,
57  std::ostream &out) const
58 {
59  out << "*** ";
60 
61  switch(type)
62  {
63  case goto_trace_stept::typet::ASSERT: out << "ASSERT"; break;
64  case goto_trace_stept::typet::ASSUME: out << "ASSUME"; break;
65  case goto_trace_stept::typet::LOCATION: out << "LOCATION"; break;
66  case goto_trace_stept::typet::ASSIGNMENT: out << "ASSIGNMENT"; break;
67  case goto_trace_stept::typet::GOTO: out << "GOTO"; break;
68  case goto_trace_stept::typet::DECL: out << "DECL"; break;
69  case goto_trace_stept::typet::DEAD: out << "DEAD"; break;
70  case goto_trace_stept::typet::OUTPUT: out << "OUTPUT"; break;
71  case goto_trace_stept::typet::INPUT: out << "INPUT"; break;
73  out << "ATOMIC_BEGIN";
74  break;
75  case goto_trace_stept::typet::ATOMIC_END: out << "ATOMIC_END"; break;
76  case goto_trace_stept::typet::SHARED_READ: out << "SHARED_READ"; break;
77  case goto_trace_stept::typet::SHARED_WRITE: out << "SHARED WRITE"; break;
78  case goto_trace_stept::typet::FUNCTION_CALL: out << "FUNCTION CALL"; break;
80  out << "FUNCTION RETURN"; break;
81  default:
82  out << "unknown type: " << static_cast<int>(type) << std::endl;
84  }
85 
86  if(is_assert() || is_assume() || is_goto())
87  out << " (" << cond_value << ')';
88  else if(is_function_call())
89  out << ' ' << called_function;
90 
91  if(hidden)
92  out << " hidden";
93 
94  out << '\n';
95 
96  if(is_assignment())
97  {
98  out << " " << format(full_lhs)
99  << " = " << format(full_lhs_value)
100  << '\n';
101  }
102 
103  if(!pc->source_location.is_nil())
104  out << pc->source_location << '\n';
105 
106  out << pc->type << '\n';
107 
108  if(pc->is_assert())
109  {
110  if(!cond_value)
111  {
112  out << "Violated property:" << '\n';
113  if(pc->source_location.is_nil())
114  out << " " << pc->source_location << '\n';
115 
116  if(!comment.empty())
117  out << " " << comment << '\n';
118 
119  out << " " << format(pc->guard) << '\n';
120  out << '\n';
121  }
122  }
123 
124  out << '\n';
125 }
135 static std::string numeric_representation(
136  const constant_exprt &expr,
137  const namespacet &ns,
138  const trace_optionst &options)
139 {
140  std::string result;
141  std::string prefix;
142 
143  const typet &expr_type = expr.type();
144 
145  const typet &underlying_type =
146  expr_type.id() == ID_c_enum_tag
147  ? ns.follow_tag(to_c_enum_tag_type(expr_type)).subtype()
148  : expr_type;
149 
150  const irep_idt &value = expr.get_value();
151 
152  const auto width = to_bitvector_type(underlying_type).get_width();
153 
154  const mp_integer value_int = bvrep2integer(id2string(value), width, false);
155 
156  if(options.hex_representation)
157  {
158  result = integer2string(value_int, 16);
159  prefix = "0x";
160  }
161  else
162  {
163  result = integer2binary(value_int, width);
164  prefix = "0b";
165  }
166 
167  std::ostringstream oss;
169  for(const auto c : result)
170  {
171  oss << c;
172  if(++i % 8 == 0 && result.size() != i)
173  oss << ' ';
174  }
175  if(options.base_prefix)
176  return prefix + oss.str();
177  else
178  return oss.str();
179 }
180 
182  const exprt &expr,
183  const namespacet &ns,
184  const trace_optionst &options)
185 {
186  const typet &type=ns.follow(expr.type());
187 
188  if(expr.id()==ID_constant)
189  {
190  if(type.id()==ID_unsignedbv ||
191  type.id()==ID_signedbv ||
192  type.id()==ID_bv ||
193  type.id()==ID_fixedbv ||
194  type.id()==ID_floatbv ||
195  type.id()==ID_pointer ||
196  type.id()==ID_c_bit_field ||
197  type.id()==ID_c_bool ||
198  type.id()==ID_c_enum ||
199  type.id()==ID_c_enum_tag)
200  {
201  return numeric_representation(to_constant_expr(expr), ns, options);
202  }
203  else if(type.id()==ID_bool)
204  {
205  return expr.is_true()?"1":"0";
206  }
207  else if(type.id()==ID_integer)
208  {
209  const auto i = numeric_cast<mp_integer>(expr);
210  if(i.has_value() && *i >= 0)
211  {
212  if(options.hex_representation)
213  return "0x" + integer2string(*i, 16);
214  else
215  return "0b" + integer2string(*i, 2);
216  }
217  }
218  }
219  else if(expr.id()==ID_array)
220  {
221  std::string result;
222 
223  forall_operands(it, expr)
224  {
225  if(result=="")
226  result="{ ";
227  else
228  result+=", ";
229  result+=trace_numeric_value(*it, ns, options);
230  }
231 
232  return result+" }";
233  }
234  else if(expr.id()==ID_struct)
235  {
236  std::string result="{ ";
237 
238  forall_operands(it, expr)
239  {
240  if(it!=expr.operands().begin())
241  result+=", ";
242  result+=trace_numeric_value(*it, ns, options);
243  }
244 
245  return result+" }";
246  }
247  else if(expr.id()==ID_union)
248  {
249  PRECONDITION(expr.operands().size()==1);
250  return trace_numeric_value(expr.op0(), ns, options);
251  }
252 
253  return "?";
254 }
255 
257  messaget::mstreamt &out,
258  const namespacet &ns,
259  const optionalt<symbol_exprt> &lhs_object,
260  const exprt &full_lhs,
261  const exprt &value,
262  const trace_optionst &options)
263 {
264  irep_idt identifier;
265 
266  if(lhs_object.has_value())
267  identifier=lhs_object->get_identifier();
268 
269  out << from_expr(ns, identifier, full_lhs) << '=';
270 
271  if(value.is_nil())
272  out << "(assignment removed)";
273  else
274  {
275  out << from_expr(ns, identifier, value);
276 
277  // the binary representation
278  out << ' ' << messaget::faint << '('
279  << trace_numeric_value(value, ns, options) << ')' << messaget::reset;
280  }
281 
282  out << '\n';
283 }
284 
285 static std::string
287 {
288  std::string result;
289 
290  const auto &source_location = state.pc->source_location;
291 
292  if(!source_location.get_file().empty())
293  result += "file " + id2string(source_location.get_file());
294 
295  if(!state.function.empty())
296  {
297  const symbolt &symbol = ns.lookup(state.function);
298  if(!result.empty())
299  result += ' ';
300  result += "function " + id2string(symbol.display_name());
301  }
302 
303  if(!source_location.get_line().empty())
304  {
305  if(!result.empty())
306  result += ' ';
307  result += "line " + id2string(source_location.get_line());
308  }
309 
310  if(!result.empty())
311  result += ' ';
312  result += "thread " + std::to_string(state.thread_nr);
313 
314  return result;
315 }
316 
318  messaget::mstreamt &out,
319  const namespacet &ns,
320  const goto_trace_stept &state,
321  unsigned step_nr,
322  const trace_optionst &options)
323 {
324  out << '\n';
325 
326  if(step_nr == 0)
327  out << "Initial State";
328  else
329  out << "State " << step_nr;
330 
331  out << ' ' << state_location(state, ns) << '\n';
332  out << "----------------------------------------------------" << '\n';
333 
334  if(options.show_code)
335  {
336  out << as_string(ns, *state.pc) << '\n';
337  out << "----------------------------------------------------" << '\n';
338  }
339 }
340 
342 {
343  if(src.id()==ID_index)
344  return is_index_member_symbol(src.op0());
345  else if(src.id()==ID_member)
346  return is_index_member_symbol(src.op0());
347  else if(src.id()==ID_symbol)
348  return true;
349  else
350  return false;
351 }
352 
359  messaget::mstreamt &out,
360  const namespacet &ns,
361  const goto_tracet &goto_trace,
362  const trace_optionst &options)
363 {
364  std::size_t function_depth = 0;
365 
366  for(const auto &step : goto_trace.steps)
367  {
368  if(step.is_function_call())
369  function_depth++;
370  else if(step.is_function_return())
371  function_depth--;
372 
373  // hide the hidden ones
374  if(step.hidden)
375  continue;
376 
377  switch(step.type)
378  {
380  if(!step.cond_value)
381  {
382  out << '\n';
383  out << messaget::red << "Violated property:" << messaget::reset << '\n';
384  if(!step.pc->source_location.is_nil())
385  out << " " << state_location(step, ns) << '\n';
386 
387  out << " " << messaget::red << step.comment << messaget::reset << '\n';
388 
389  if(step.pc->is_assert())
390  out << " " << from_expr(ns, step.function, step.pc->guard) << '\n';
391 
392  out << '\n';
393  }
394  break;
395 
397  if(
398  step.assignment_type ==
400  {
401  break;
402  }
403 
404  out << " ";
405 
406  if(!step.pc->source_location.get_line().empty())
407  {
408  out << messaget::faint << step.pc->source_location.get_line() << ':'
409  << messaget::reset << ' ';
410  }
411 
412  trace_value(
413  out,
414  ns,
415  step.get_lhs_object(),
416  step.full_lhs,
417  step.full_lhs_value,
418  options);
419  break;
420 
422  // downwards arrow
423  out << '\n' << messaget::faint << u8"\u21b3" << messaget::reset << ' ';
424  if(!step.pc->source_location.get_file().empty())
425  {
426  out << messaget::faint << step.pc->source_location.get_file();
427 
428  if(!step.pc->source_location.get_line().empty())
429  {
430  out << messaget::faint << ':' << step.pc->source_location.get_line();
431  }
432 
433  out << messaget::reset << ' ';
434  }
435 
436  {
437  // show the display name
438  const auto &f_symbol = ns.lookup(step.called_function);
439  out << f_symbol.display_name();
440  }
441 
442  {
443  auto arg_strings = make_range(step.function_arguments)
444  .map([&ns, &step](const exprt &arg) {
445  return from_expr(ns, step.function, arg);
446  });
447 
448  out << '(';
449  join_strings(out, arg_strings.begin(), arg_strings.end(), ", ");
450  out << ")\n";
451  }
452 
453  break;
454 
456  // upwards arrow
457  out << messaget::faint << u8"\u21b5" << messaget::reset << '\n';
458  break;
459 
471  break;
472 
473  default:
474  UNREACHABLE;
475  }
476  }
477 }
478 
480  messaget::mstreamt &out,
481  const namespacet &ns,
482  const goto_tracet &goto_trace,
483  const trace_optionst &options)
484 {
485  unsigned prev_step_nr=0;
486  bool first_step=true;
487  std::size_t function_depth=0;
488 
489  for(const auto &step : goto_trace.steps)
490  {
491  // hide the hidden ones
492  if(step.hidden)
493  continue;
494 
495  switch(step.type)
496  {
498  if(!step.cond_value)
499  {
500  out << '\n';
501  out << messaget::red << "Violated property:" << messaget::reset << '\n';
502  if(!step.pc->source_location.is_nil())
503  {
504  out << " " << state_location(step, ns) << '\n';
505  }
506 
507  out << " " << messaget::red << step.comment << messaget::reset << '\n';
508 
509  if(step.pc->is_assert())
510  out << " " << from_expr(ns, step.function, step.pc->guard) << '\n';
511 
512  out << '\n';
513  }
514  break;
515 
517  if(!step.cond_value)
518  {
519  out << '\n';
520  out << "Violated assumption:" << '\n';
521  if(!step.pc->source_location.is_nil())
522  out << " " << step.pc->source_location << '\n';
523 
524  if(step.pc->is_assume())
525  out << " " << from_expr(ns, step.function, step.pc->guard) << '\n';
526 
527  out << '\n';
528  }
529  break;
530 
532  break;
533 
535  break;
536 
538  if(step.pc->is_assign() ||
539  step.pc->is_return() || // returns have a lhs!
540  step.pc->is_function_call() ||
541  (step.pc->is_other() && step.full_lhs.is_not_nil()))
542  {
543  if(prev_step_nr!=step.step_nr || first_step)
544  {
545  first_step=false;
546  prev_step_nr=step.step_nr;
547  show_state_header(out, ns, step, step.step_nr, options);
548  }
549 
550  out << " ";
551  trace_value(
552  out,
553  ns,
554  step.get_lhs_object(),
555  step.full_lhs,
556  step.full_lhs_value,
557  options);
558  }
559  break;
560 
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, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
572  break;
573 
575  if(step.formatted)
576  {
577  printf_formattert printf_formatter(ns);
578  printf_formatter(id2string(step.format_string), step.io_args);
579  printf_formatter.print(out);
580  out << '\n';
581  }
582  else
583  {
584  show_state_header(out, ns, step, step.step_nr, options);
585  out << " OUTPUT " << step.io_id << ':';
586 
587  for(std::list<exprt>::const_iterator
588  l_it=step.io_args.begin();
589  l_it!=step.io_args.end();
590  l_it++)
591  {
592  if(l_it!=step.io_args.begin())
593  out << ';';
594 
595  out << ' ' << from_expr(ns, step.function, *l_it);
596 
597  // the binary representation
598  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
599  }
600 
601  out << '\n';
602  }
603  break;
604 
606  show_state_header(out, ns, step, step.step_nr, options);
607  out << " INPUT " << step.io_id << ':';
608 
609  for(std::list<exprt>::const_iterator
610  l_it=step.io_args.begin();
611  l_it!=step.io_args.end();
612  l_it++)
613  {
614  if(l_it!=step.io_args.begin())
615  out << ';';
616 
617  out << ' ' << from_expr(ns, step.function, *l_it);
618 
619  // the binary representation
620  out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
621  }
622 
623  out << '\n';
624  break;
625 
627  function_depth++;
628  if(options.show_function_calls)
629  {
630  out << "\n#### Function call: " << step.called_function;
631  out << '(';
632 
633  bool first = true;
634  for(auto &arg : step.function_arguments)
635  {
636  if(first)
637  first = false;
638  else
639  out << ", ";
640 
641  out << from_expr(ns, step.function, arg);
642  }
643 
644  out << ") (depth " << function_depth << ") ####\n";
645  }
646  break;
647 
649  function_depth--;
650  if(options.show_function_calls)
651  {
652  out << "\n#### Function return from " << step.function << " (depth "
653  << function_depth << ") ####\n";
654  }
655  break;
656 
662  break;
663 
667  default:
668  UNREACHABLE;
669  }
670  }
671 }
672 
674  messaget::mstreamt &out,
675  const namespacet &ns,
676  const goto_tracet &goto_trace)
677 {
678  // map from thread number to a call stack
679  std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
680  call_stacks;
681 
682  // by default, we show thread 0
683  unsigned thread_to_show = 0;
684 
685  for(auto s_it = goto_trace.steps.begin(); s_it != goto_trace.steps.end();
686  s_it++)
687  {
688  const auto &step = *s_it;
689  auto &stack = call_stacks[step.thread_nr];
690 
691  if(step.is_assert())
692  {
693  if(!step.cond_value)
694  {
695  stack.push_back(s_it);
696  thread_to_show = step.thread_nr;
697  }
698  }
699  else if(step.is_function_call())
700  {
701  stack.push_back(s_it);
702  }
703  else if(step.is_function_return())
704  {
705  stack.pop_back();
706  }
707  }
708 
709  const auto &stack = call_stacks[thread_to_show];
710 
711  // print in reverse order
712  for(auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
713  {
714  const auto &step = **s_it;
715  if(step.is_assert())
716  {
717  out << " assertion failure";
718  if(!step.pc->source_location.is_nil())
719  out << ' ' << step.pc->source_location;
720  out << '\n';
721  }
722  else if(step.is_function_call())
723  {
724  out << " " << step.called_function;
725  out << '(';
726 
727  bool first = true;
728  for(auto &arg : step.function_arguments)
729  {
730  if(first)
731  first = false;
732  else
733  out << ", ";
734 
735  out << from_expr(ns, step.function, arg);
736  }
737 
738  out << ')';
739 
740  if(!step.pc->source_location.is_nil())
741  out << ' ' << step.pc->source_location;
742 
743  out << '\n';
744  }
745  }
746 }
747 
749  messaget::mstreamt &out,
750  const namespacet &ns,
751  const goto_tracet &goto_trace,
752  const trace_optionst &options)
753 {
754  if(options.stack_trace)
755  show_goto_stack_trace(out, ns, goto_trace);
756  else if(options.compact_trace)
757  show_compact_goto_trace(out, ns, goto_trace, options);
758  else
759  show_full_goto_trace(out, ns, goto_trace, options);
760 }
761 
763  messaget::mstreamt &out,
764  const namespacet &ns,
765  const goto_tracet &goto_trace)
766 {
767  show_goto_trace(out, ns, goto_trace, trace_optionst::default_options);
768 }
769 
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:737
trace_optionst::compact_trace
bool compact_trace
Definition: goto_trace.h:203
format
static format_containert< T > format(const T &o)
Definition: format.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
goto_trace_stept::typet::LOCATION
@ LOCATION
goto_trace_stept::full_lhs_value
exprt full_lhs_value
Definition: goto_trace.h:111
typet::subtype
const typet & subtype() const
Definition: type.h:38
goto_trace_stept::get_lhs_object
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:42
goto_trace_stept::comment
std::string comment
Definition: goto_trace.h:102
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:479
goto_trace_stept::typet::ASSUME
@ ASSUME
trace_value
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:256
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:330
printf_formatter.h
string_utils.h
trace_optionst::base_prefix
bool base_prefix
Definition: goto_trace.h:200
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:27
state_location
static std::string state_location(const goto_trace_stept &state, const namespacet &ns)
Definition: goto_trace.cpp:286
u8
uint64_t u8
Definition: bytecode_info.h:58
trace_optionst::show_code
bool show_code
Definition: goto_trace.h:202
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
goto_trace_stept::is_assert
bool is_assert() const
Definition: goto_trace.h:37
goto_trace_stept::type
typet type
Definition: goto_trace.h:77
goto_tracet::steps
stepst steps
Definition: goto_trace.h:154
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::op0
exprt & op0()
Definition: expr.h:84
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
goto_trace_stept
TO_BE_DOCUMENTED.
Definition: goto_trace.h:30
goto_trace_stept::function
irep_idt function
Definition: goto_trace.h:91
goto_trace_stept::is_function_call
bool is_function_call() const
Definition: goto_trace.h:40
goto_trace_stept::called_function
irep_idt called_function
Definition: goto_trace.h:120
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
join_strings
Stream & join_strings(Stream &os, const It b, const It e, const Delimiter &delimiter)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:52
goto_trace_stept::is_assignment
bool is_assignment() const
Definition: goto_trace.h:35
goto_trace.h
printf_formattert::print
void print(std::ostream &out)
Definition: printf_formatter.cpp:39
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
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:358
messaget::faint
static const commandt faint
render text with faint font
Definition: message.h:372
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:55
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:236
namespace_baset::follow_tag
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
language_util.h
goto_trace_stept::full_lhs
exprt full_lhs
Definition: goto_trace.h:105
goto_trace_stept::pc
goto_programt::const_targett pc
Definition: goto_trace.h:92
is_index_member_symbol
bool is_index_member_symbol(const exprt &src)
Definition: goto_trace.cpp:341
get_object_rec
static optionalt< symbol_exprt > get_object_rec(const exprt &src)
Definition: goto_trace.cpp:28
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:47
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
symbol.h
Symbol table entry.
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
range.h
dstringt::empty
bool empty() const
Definition: dstring.h:75
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:95
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:317
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1117
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
as_string
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
Definition: goto_program.cpp:403
goto_trace_stept::cond_value
bool cond_value
Definition: goto_trace.h:98
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:425
trace_optionst::hex_representation
bool hex_representation
Definition: goto_trace.h:199
trace_optionst::stack_trace
bool stack_trace
Definition: goto_trace.h:204
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)
Definition: goto_trace.cpp:748
messaget::red
static const commandt red
render text with red foreground color
Definition: message.h:333
trace_optionst
Definition: goto_trace.h:196
trace_optionst::show_function_calls
bool show_function_calls
Definition: goto_trace.h:201
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
trace_optionst::default_options
static const trace_optionst default_options
Definition: goto_trace.h:206
stack
#define stack(x)
Definition: parser.h:144
symbolt
Symbol table entry.
Definition: symbol.h:27
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:135
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
goto_trace_stept::hidden
bool hidden
Definition: goto_trace.h:80
trace_numeric_value
std::string trace_numeric_value(const exprt &expr, const namespacet &ns, const trace_optionst &options)
Definition: goto_trace.cpp:181
goto_tracet
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
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:673
messaget::mstreamt
Definition: message.h:212
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
goto_trace_stept::is_assume
bool is_assume() const
Definition: goto_trace.h:36
exprt::operands
operandst & operands()
Definition: expr.h:78
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
goto_trace_stept::is_goto
bool is_goto() const
Definition: goto_trace.h:38
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:4384
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:4403
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:384
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:1158
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:4423
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106