30 if(src.
id()==ID_symbol)
32 else if(src.
id()==ID_member)
34 else if(src.
id()==ID_index)
36 else if(src.
id()==ID_typecast)
49 std::ostream &out)
const 51 for(
const auto &step :
steps)
57 std::ostream &out)
const 73 out <<
"ATOMIC_BEGIN";
80 out <<
"FUNCTION RETURN";
break;
82 out <<
"unknown type: " << static_cast<int>(
type) << std::endl;
103 if(!
pc->source_location.is_nil())
104 out <<
pc->source_location <<
'\n';
106 out <<
pc->type <<
'\n';
112 out <<
"Violated property:" <<
'\n';
113 if(
pc->source_location.is_nil())
114 out <<
" " <<
pc->source_location <<
'\n';
119 out <<
" " <<
format(
pc->guard) <<
'\n';
145 const typet &underlying_type =
146 expr_type.
id() == ID_c_enum_tag
167 std::ostringstream oss;
169 for(
const auto c : result)
172 if(++i % 8 == 0 && result.size() != i)
176 return prefix + oss.str();
188 if(expr.
id()==ID_constant)
190 if(type.
id()==ID_unsignedbv ||
191 type.
id()==ID_signedbv ||
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)
203 else if(type.
id()==ID_bool)
207 else if(type.
id()==ID_integer)
209 const auto i = numeric_cast<mp_integer>(expr);
210 if(i.has_value() && *i >= 0)
219 else if(expr.
id()==ID_array)
234 else if(expr.
id()==ID_struct)
236 std::string result=
"{ ";
247 else if(expr.
id()==ID_union)
260 const exprt &full_lhs,
266 if(lhs_object.has_value())
267 identifier=lhs_object->get_identifier();
269 out <<
from_expr(ns, identifier, full_lhs) <<
'=';
272 out <<
"(assignment removed)";
290 const auto &source_location = state.
pc->source_location;
292 if(!source_location.get_file().empty())
293 result +=
"file " +
id2string(source_location.get_file());
303 if(!source_location.get_line().empty())
307 result +=
"line " +
id2string(source_location.get_line());
327 out <<
"Initial State";
329 out <<
"State " << step_nr;
332 out <<
"----------------------------------------------------" <<
'\n';
337 out <<
"----------------------------------------------------" <<
'\n';
343 if(src.
id()==ID_index)
345 else if(src.
id()==ID_member)
347 else if(src.
id()==ID_symbol)
364 std::size_t function_depth = 0;
366 for(
const auto &step : goto_trace.
steps)
368 if(step.is_function_call())
370 else if(step.is_function_return())
384 if(!step.pc->source_location.is_nil())
389 if(step.pc->is_assert())
390 out <<
" " <<
from_expr(ns, step.function, step.pc->guard) <<
'\n';
398 step.assignment_type ==
406 if(!step.pc->source_location.get_line().empty())
415 step.get_lhs_object(),
424 if(!step.pc->source_location.get_file().empty())
428 if(!step.pc->source_location.get_line().empty())
438 const auto &f_symbol = ns.
lookup(step.called_function);
439 out << f_symbol.display_name();
443 auto arg_strings =
make_range(step.function_arguments)
444 .map([&ns, &step](
const exprt &arg) {
445 return from_expr(ns, step.function, arg);
449 join_strings(out, arg_strings.begin(), arg_strings.end(),
", ");
485 unsigned prev_step_nr=0;
486 bool first_step=
true;
487 std::size_t function_depth=0;
489 for(
const auto &step : goto_trace.
steps)
502 if(!step.pc->source_location.is_nil())
509 if(step.pc->is_assert())
510 out <<
" " <<
from_expr(ns, step.function, step.pc->guard) <<
'\n';
520 out <<
"Violated assumption:" <<
'\n';
521 if(!step.pc->source_location.is_nil())
524 if(step.pc->is_assume())
525 out <<
" " <<
from_expr(ns, step.function, step.pc->guard) <<
'\n';
538 if(step.pc->is_assign() ||
539 step.pc->is_return() ||
540 step.pc->is_function_call() ||
541 (step.pc->is_other() && step.full_lhs.is_not_nil()))
543 if(prev_step_nr!=step.step_nr || first_step)
546 prev_step_nr=step.step_nr;
554 step.get_lhs_object(),
562 if(prev_step_nr!=step.step_nr || first_step)
565 prev_step_nr=step.step_nr;
571 out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
578 printf_formatter(
id2string(step.format_string), step.io_args);
579 printf_formatter.
print(out);
585 out <<
" OUTPUT " << step.io_id <<
':';
587 for(std::list<exprt>::const_iterator
588 l_it=step.io_args.begin();
589 l_it!=step.io_args.end();
592 if(l_it!=step.io_args.begin())
595 out <<
' ' <<
from_expr(ns, step.function, *l_it);
607 out <<
" INPUT " << step.io_id <<
':';
609 for(std::list<exprt>::const_iterator
610 l_it=step.io_args.begin();
611 l_it!=step.io_args.end();
614 if(l_it!=step.io_args.begin())
617 out <<
' ' <<
from_expr(ns, step.function, *l_it);
630 out <<
"\n#### Function call: " << step.called_function;
634 for(
auto &arg : step.function_arguments)
641 out <<
from_expr(ns, step.function, arg);
644 out <<
") (depth " << function_depth <<
") ####\n";
652 out <<
"\n#### Function return from " << step.function <<
" (depth " 653 << function_depth <<
") ####\n";
679 std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
683 unsigned thread_to_show = 0;
685 for(
auto s_it = goto_trace.
steps.begin(); s_it != goto_trace.
steps.end();
688 const auto &step = *s_it;
689 auto &
stack = call_stacks[step.thread_nr];
695 stack.push_back(s_it);
696 thread_to_show = step.thread_nr;
699 else if(step.is_function_call())
701 stack.push_back(s_it);
703 else if(step.is_function_return())
709 const auto &
stack = call_stacks[thread_to_show];
712 for(
auto s_it =
stack.rbegin(); s_it !=
stack.rend(); s_it++)
714 const auto &step = **s_it;
717 out <<
" assertion failure";
718 if(!step.pc->source_location.is_nil())
722 else if(step.is_function_call())
724 out <<
" " << step.called_function;
728 for(
auto &arg : step.function_arguments)
735 out <<
from_expr(ns, step.function, arg);
740 if(!step.pc->source_location.is_nil())
The type of an expression, extends irept.
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
const std::string & id2string(const irep_idt &d)
const std::string integer2string(const mp_integer &n, unsigned base)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::string trace_numeric_value(const exprt &expr, const namespacet &ns, const trace_optionst &options)
void show_state_header(messaget::mstreamt &out, const namespacet &ns, const goto_trace_stept &state, unsigned step_nr, const trace_optionst &options)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const irep_idt & get_value() const
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
unsignedbv_typet size_type()
A constant literal expression.
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
static const commandt reset
return to default formatting, as defined by the terminal
goto_programt::const_targett pc
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Stream & join_strings(Stream &os, const It b, const It e, const Delimiter &delimiter)
Prints items to an stream, separated by a constant delimiter.
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace in ASCII to a given stream
void output(const class namespacet &ns, std::ostream &out) const
outputs the trace step in ASCII to a given stream
bool is_function_call() const
const irep_idt & id() const
bool is_index_member_symbol(const exprt &src)
static std::string state_location(const goto_trace_stept &state, const namespacet &ns)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
source_locationt source_location
nonstd::optional< T > optionalt
static const commandt red
render text with red foreground color
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
optionalt< symbol_exprt > get_lhs_object() const
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
ranget< iteratort > make_range(iteratort begin, iteratort end)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
std::size_t get_width() const
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
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)
const irep_idt & display_name() const
Return language specific display name if present.
static const commandt faint
render text with faint font
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
void show_full_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, 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.
Base class for all expressions.
const exprt & struct_op() const
const std::string integer2binary(const mp_integer &n, std::size_t width)
#define UNREACHABLE
This should be used to mark dead code.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool is_assignment() const
static void show_goto_stack_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace)
static optionalt< symbol_exprt > get_object_rec(const exprt &src)
static const trace_optionst default_options
const typet & subtype() const
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().