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