Go to the documentation of this file.
33 if(src.
id()==ID_symbol)
35 else if(src.
id()==ID_member)
37 else if(src.
id()==ID_index)
39 else if(src.
id()==ID_typecast)
42 src.
id() == ID_byte_extract_little_endian ||
43 src.
id() == ID_byte_extract_big_endian)
58 std::ostream &out)
const
60 for(
const auto &step :
steps)
66 std::ostream &out)
const
83 out <<
"ATOMIC_BEGIN";
90 out <<
"FUNCTION RETURN";
break;
115 if(!
pc->source_location.is_nil())
116 out <<
pc->source_location <<
'\n';
118 out <<
pc->type <<
'\n';
124 out <<
"Violated property:" <<
'\n';
125 if(
pc->source_location.is_nil())
126 out <<
" " <<
pc->source_location <<
'\n';
131 out <<
" " <<
format(
pc->get_condition()) <<
'\n';
171 const typet &underlying_type =
172 expr_type.
id() == ID_c_enum_tag
193 std::ostringstream oss;
195 for(
const auto c : result)
198 if(++i % 8 == 0 && result.size() != i)
202 return prefix + oss.str();
214 if(expr.
id()==ID_constant)
216 if(type.
id()==ID_unsignedbv ||
217 type.
id()==ID_signedbv ||
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)
229 else if(type.
id()==ID_bool)
233 else if(type.
id()==ID_integer)
235 const auto i = numeric_cast<mp_integer>(expr);
236 if(i.has_value() && *i >= 0)
245 else if(expr.
id()==ID_array)
260 else if(expr.
id()==ID_struct)
262 std::string result=
"{ ";
273 else if(expr.
id()==ID_union)
285 const exprt &full_lhs,
291 if(lhs_object.has_value())
292 identifier=lhs_object->get_identifier();
294 out <<
from_expr(ns, identifier, full_lhs) <<
'=';
297 out <<
"(assignment removed)";
315 const auto &source_location = state.
pc->source_location;
317 if(!source_location.get_file().empty())
318 result +=
"file " +
id2string(source_location.get_file());
328 if(!source_location.get_line().empty())
332 result +=
"line " +
id2string(source_location.get_line());
352 out <<
"Initial State";
354 out <<
"State " << step_nr;
357 out <<
"----------------------------------------------------" <<
'\n';
362 out <<
"----------------------------------------------------" <<
'\n';
368 if(src.
id()==ID_index)
370 else if(src.
id()==ID_member)
372 else if(src.
id()==ID_symbol)
389 std::size_t function_depth = 0;
391 for(
const auto &step : goto_trace.
steps)
393 if(step.is_function_call())
395 else if(step.is_function_return())
409 if(!step.pc->source_location.is_nil())
414 if(step.pc->is_assert())
417 <<
from_expr(ns, step.function_id, step.pc->get_condition())
427 step.assignment_type ==
435 if(!step.pc->source_location.get_line().empty())
444 step.get_lhs_object(),
453 if(!step.pc->source_location.get_file().empty())
457 if(!step.pc->source_location.get_line().empty())
467 const auto &f_symbol = ns.
lookup(step.called_function);
468 out << f_symbol.display_name();
472 auto arg_strings =
make_range(step.function_arguments)
473 .map([&ns, &step](
const exprt &arg) {
474 return from_expr(ns, step.function_id, arg);
478 join_strings(out, arg_strings.begin(), arg_strings.end(),
", ");
517 unsigned prev_step_nr=0;
518 bool first_step=
true;
519 std::size_t function_depth=0;
521 for(
const auto &step : goto_trace.
steps)
534 if(!step.pc->source_location.is_nil())
541 if(step.pc->is_assert())
544 <<
from_expr(ns, step.function_id, step.pc->get_condition())
553 if(step.cond_value && step.pc->is_assume())
556 out <<
"Assumption:\n";
558 if(!step.pc->source_location.is_nil())
561 out <<
" " <<
from_expr(ns, step.function_id, step.pc->get_condition())
573 if(step.pc->is_assign() ||
574 step.pc->is_return() ||
575 step.pc->is_function_call() ||
576 (step.pc->is_other() && step.full_lhs.is_not_nil()))
578 if(prev_step_nr!=step.step_nr || first_step)
581 prev_step_nr=step.step_nr;
589 step.get_lhs_object(),
597 if(prev_step_nr!=step.step_nr || first_step)
600 prev_step_nr=step.step_nr;
606 out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
613 printf_formatter(
id2string(step.format_string), step.io_args);
614 printf_formatter.
print(out);
620 out <<
" OUTPUT " << step.io_id <<
':';
622 for(std::list<exprt>::const_iterator
623 l_it=step.io_args.begin();
624 l_it!=step.io_args.end();
627 if(l_it!=step.io_args.begin())
630 out <<
' ' <<
from_expr(ns, step.function_id, *l_it);
642 out <<
" INPUT " << step.io_id <<
':';
644 for(std::list<exprt>::const_iterator
645 l_it=step.io_args.begin();
646 l_it!=step.io_args.end();
649 if(l_it!=step.io_args.begin())
652 out <<
' ' <<
from_expr(ns, step.function_id, *l_it);
665 out <<
"\n#### Function call: " << step.called_function;
669 for(
auto &arg : step.function_arguments)
676 out <<
from_expr(ns, step.function_id, arg);
679 out <<
") (depth " << function_depth <<
") ####\n";
687 out <<
"\n#### Function return from " << step.function_id <<
" (depth "
688 << function_depth <<
") ####\n";
714 std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
718 unsigned thread_to_show = 0;
720 for(
auto s_it = goto_trace.
steps.begin(); s_it != goto_trace.
steps.end();
723 const auto &step = *s_it;
724 auto &stack = call_stacks[step.thread_nr];
730 stack.push_back(s_it);
731 thread_to_show = step.thread_nr;
734 else if(step.is_function_call())
736 stack.push_back(s_it);
738 else if(step.is_function_return())
744 const auto &stack = call_stacks[thread_to_show];
747 for(
auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
749 const auto &step = **s_it;
752 out <<
" assertion failure";
753 if(!step.pc->source_location.is_nil())
757 else if(step.is_function_call())
759 out <<
" " << step.called_function;
763 for(
auto &arg : step.function_arguments)
770 out <<
from_expr(ns, step.function_id, arg);
775 if(!step.pc->source_location.is_nil())
801 std::set<irep_idt> property_ids;
802 for(
const auto &step :
steps)
804 if(step.is_assert() && !step.cond_value)
805 property_ids.insert(step.property_id);
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool compact_trace
Give a compact trace.
std::set< irep_idt > get_failed_property_ids() const
Returns the property IDs of all failed assertions in the trace.
const typet & subtype() const
optionalt< symbol_exprt > get_lhs_object() const
void show_full_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
static const commandt reset
return to default formatting, as defined by the terminal
bool base_prefix
Use prefix (0b or 0x) for distinguishing the base of the representation.
const irep_idt & display_name() const
Return language specific display name if present.
The type of an expression, extends irept.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
static std::string state_location(const goto_trace_stept &state, const namespacet &ns)
bool show_code
Show original code in plain text trace.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Base class for all expressions.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool is_true() const
Return whether the expression is a constant representing true.
Step of the trace of a GOTO program.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
bool is_function_call() const
bool is_assignment() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression classes for byte-level operators.
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
static const commandt faint
render text with faint font
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace step in ASCII to a given stream.
const std::string & id2string(const irep_idt &d)
source_locationt source_location
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
#define forall_operands(it, expr)
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.
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)
std::vector< exprt > function_arguments
goto_programt::const_targett pc
bool is_index_member_symbol(const exprt &src)
static optionalt< symbol_exprt > get_object_rec(const exprt &src)
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace in ASCII to a given stream.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
Ranges: pair of begin and end iterators, which can be initialized from containers,...
nonstd::optional< T > optionalt
void show_state_header(messaget::mstreamt &out, const namespacet &ns, const goto_trace_stept &state, unsigned step_nr, const trace_optionst &options)
std::size_t get_width() const
void merge_ireps(merge_irept &dest)
Use dest to establish sharing among ireps.
bool hex_representation
Represent plain trace values in hex.
bool stack_trace
Give a stack trace only.
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 const commandt red
render text with red foreground color
Options for printing the trace using show_goto_trace.
bool show_function_calls
Show function calls in plain text trace.
static const trace_optionst default_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.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
std::string trace_numeric_value(const exprt &expr, const namespacet &ns, const trace_optionst &options)
static void show_goto_stack_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace)
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const std::string integer2binary(const mp_integer &n, std::size_t width)
unsignedbv_typet size_type()
A constant literal expression.
const irep_idt & get_value() const
ranget< iteratort > make_range(iteratort begin, iteratort end)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)