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