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 =
193 std::ostringstream
oss;
194 std::string::size_type
i = 0;
195 for(
const auto c : result)
198 if(++
i % 8 == 0 && result.size() !=
i)
202 return prefix +
oss.str();
236 if(
i.has_value() && *
i >= 0)
262 std::string result=
"{ ";
285 const exprt &full_lhs,
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());
337 result +=
"thread " + std::to_string(state.
thread_nr);
352 out <<
"Initial State";
354 out <<
"State " << step_nr;
357 out <<
"----------------------------------------------------" <<
'\n';
362 out <<
"----------------------------------------------------" <<
'\n';
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())
460 << step.pc->source_location().get_line();
474 .map([&ns, &step](
const exprt &arg) {
475 return from_expr(ns, step.function_id, arg);
535 if(!step.pc->source_location().is_nil())
542 if(step.pc->is_assert())
545 <<
from_expr(ns, step.function_id, step.pc->get_condition())
554 if(step.cond_value && step.pc->is_assume())
557 out <<
"Assumption:\n";
559 if(!step.pc->source_location().is_nil())
562 out <<
" " <<
from_expr(ns, step.function_id, step.pc->get_condition())
575 step.pc->is_assign() ||
576 step.pc->is_set_return_value() ||
577 step.pc->is_function_call() ||
578 (step.pc->is_other() && step.full_lhs.is_not_nil()))
591 step.get_lhs_object(),
608 out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
622 out <<
" OUTPUT " << step.io_id <<
':';
624 for(std::list<exprt>::const_iterator
625 l_it=step.io_args.begin();
626 l_it!=step.io_args.end();
629 if(
l_it!=step.io_args.begin())
644 out <<
" INPUT " << step.io_id <<
':';
646 for(std::list<exprt>::const_iterator
647 l_it=step.io_args.begin();
648 l_it!=step.io_args.end();
651 if(
l_it!=step.io_args.begin())
667 out <<
"\n#### Function call: " << step.called_function;
671 for(
auto &arg : step.function_arguments)
678 out <<
from_expr(ns, step.function_id, arg);
689 out <<
"\n#### Function return from " << step.function_id <<
" (depth "
716 std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
725 const auto &step = *
s_it;
732 stack.push_back(
s_it);
736 else if(step.is_function_call())
738 stack.push_back(
s_it);
740 else if(step.is_function_return())
749 for(
auto s_it = stack.rbegin();
s_it != stack.rend();
s_it++)
751 const auto &step = **
s_it;
754 out <<
" assertion failure";
755 if(!step.pc->source_location().is_nil())
759 else if(step.is_function_call())
761 out <<
" " << step.called_function;
765 for(
auto &arg : step.function_arguments)
772 out <<
from_expr(ns, step.function_id, arg);
777 if(!step.pc->source_location().is_nil())
803 std::set<irep_idt> property_ids;
804 for(
const auto &step :
steps)
806 if(step.is_assert() && !step.cond_value)
807 property_ids.insert(step.property_id);
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)
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::size_t get_width() const
A constant literal expression.
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
Step of the trace of a GOTO program.
std::vector< exprt > function_arguments
bool is_function_call() const
optionalt< symbol_exprt > get_lhs_object() const
bool is_assignment() const
goto_programt::const_targett pc
void merge_ireps(merge_irept &dest)
Use dest to establish sharing among ireps.
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace step in ASCII to a given stream.
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
source_locationt source_location
static const commandt reset
return to default formatting, as defined by the terminal
static const commandt faint
render text with faint font
static const commandt red
render text with red foreground color
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const irep_idt & display_name() const
Return language specific display name if present.
The type of an expression, extends irept.
#define forall_operands(it, expr)
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
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
const std::string integer2string(const mp_integer &n, unsigned base)
const std::string integer2binary(const mp_integer &n, std::size_t width)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
#define UNREACHABLE
This should be used to mark dead code.
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.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
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.
Options for printing the trace using show_goto_trace.
static const trace_optionst default_options
bool hex_representation
Represent plain trace values in hex.
bool base_prefix
Use prefix (0b or 0x) for distinguishing the base of the representation.
bool show_code
Show original code in plain text trace.
bool compact_trace
Give a compact trace.
bool show_function_calls
Show function calls in plain text trace.
bool stack_trace
Give a stack trace only.