60 std::ostream &out)
const
62 for(
const auto &step :
steps)
68 std::ostream &out)
const
85 out <<
"ATOMIC_BEGIN";
92 out <<
"FUNCTION RETURN";
break;
117 if(!
pc->source_location().is_nil())
118 out <<
pc->source_location() <<
'\n';
120 out <<
pc->type() <<
'\n';
126 out <<
"Violated property:" <<
'\n';
127 if(
pc->source_location().is_nil())
128 out <<
" " <<
pc->source_location() <<
'\n';
173 const typet &underlying_type =
195 std::ostringstream
oss;
196 std::string::size_type i = 0;
197 for(
const auto c : result)
200 if(++i %
config.
ansi_c.char_width == 0 && result.size() != i)
204 return prefix +
oss.str();
238 if(i.has_value() && *i >= 0)
260 for(
const auto &op : expr.
operands())
273 std::string result=
"{ ";
296 const exprt &full_lhs,
305 out <<
from_expr(ns, identifier, full_lhs) <<
'=';
308 out <<
"(assignment removed)";
326 const auto &source_location = state.
pc->source_location();
328 if(!source_location.get_file().empty())
329 result +=
"file " +
id2string(source_location.get_file());
339 if(!source_location.get_line().empty())
343 result +=
"line " +
id2string(source_location.get_line());
348 result +=
"thread " + std::to_string(state.
thread_nr);
363 out <<
"Initial State";
365 out <<
"State " << step_nr;
368 out <<
"----------------------------------------------------" <<
'\n';
373 out <<
"----------------------------------------------------" <<
'\n';
413 if(!step.pc->source_location().is_nil())
418 if(step.pc->is_assert())
421 <<
from_expr(ns, step.function_id, step.original_condition)
431 step.assignment_type ==
439 if(!step.pc->source_location().get_line().empty())
448 step.get_lhs_object(),
457 if(!step.pc->source_location().get_file().empty())
461 if(!step.pc->source_location().get_line().empty())
464 << step.pc->source_location().get_line();
478 .map([&ns, &step](
const exprt &arg) {
479 return from_expr(ns, step.function_id, arg);
539 if(!step.pc->source_location().is_nil())
546 if(step.pc->is_assert())
549 <<
from_expr(ns, step.function_id, step.original_condition)
558 if(step.cond_value && step.pc->is_assume())
561 out <<
"Assumption:\n";
563 if(!step.pc->source_location().is_nil())
566 out <<
" " <<
from_expr(ns, step.function_id, step.original_condition)
579 step.pc->is_assign() ||
580 step.pc->is_set_return_value() ||
581 step.pc->is_function_call() ||
582 (step.pc->is_other() && step.full_lhs.is_not_nil()))
595 step.get_lhs_object(),
612 out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
626 out <<
" OUTPUT " << step.io_id <<
':';
628 for(std::list<exprt>::const_iterator
629 l_it=step.io_args.begin();
630 l_it!=step.io_args.end();
633 if(
l_it!=step.io_args.begin())
648 out <<
" INPUT " << step.io_id <<
':';
650 for(std::list<exprt>::const_iterator
651 l_it=step.io_args.begin();
652 l_it!=step.io_args.end();
655 if(
l_it!=step.io_args.begin())
671 out <<
"\n#### Function call: " << step.called_function;
675 for(
auto &arg : step.function_arguments)
682 out <<
from_expr(ns, step.function_id, arg);
693 out <<
"\n#### Function return from " << step.function_id <<
" (depth "
720 std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
729 const auto &step = *
s_it;
736 stack.push_back(
s_it);
740 else if(step.is_function_call())
742 stack.push_back(
s_it);
744 else if(step.is_function_return())
753 for(
auto s_it = stack.rbegin();
s_it != stack.rend();
s_it++)
755 const auto &step = **
s_it;
758 out <<
" assertion failure";
759 if(!step.pc->source_location().is_nil())
763 else if(step.is_function_call())
765 out <<
" " << step.called_function;
769 for(
auto &arg : step.function_arguments)
776 out <<
from_expr(ns, step.function_id, arg);
781 if(!step.pc->source_location().is_nil())
807 std::set<irep_idt> property_ids;
808 for(
const auto &step :
steps)
810 if(step.is_assert() && !step.cond_value)
811 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...
struct configt::ansi_ct ansi_c
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.
bool is_constant() const
Return whether the expression is a constant.
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.
Fixed-width bit-vector with unsigned binary interpretation.
#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)
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.
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.