29 std::ostream &out)
const 31 for(
const auto &step :
steps)
37 std::ostream &out)
const 53 out <<
"ATOMIC_BEGIN";
60 out <<
"FUNCTION RETURN";
break;
62 out <<
"unknown type: " <<
static_cast<int>(
type) << std::endl;
83 if(!
pc->source_location.is_nil())
84 out <<
pc->source_location <<
'\n';
86 out <<
pc->type <<
'\n';
92 out <<
"Violated property:" <<
'\n';
93 if(
pc->source_location.is_nil())
94 out <<
" " <<
pc->source_location <<
'\n';
99 out <<
" " <<
format(
pc->guard) <<
'\n';
132 std::ostringstream oss;
134 for(
const auto c : result)
137 if(++i % 8 == 0 && result.size() != i)
141 return prefix + oss.str();
153 if(expr.
id()==ID_constant)
155 if(type.
id()==ID_unsignedbv ||
156 type.
id()==ID_signedbv ||
158 type.
id()==ID_fixedbv ||
159 type.
id()==ID_floatbv ||
160 type.
id()==ID_pointer ||
161 type.
id()==ID_c_bit_field ||
162 type.
id()==ID_c_bool ||
163 type.
id()==ID_c_enum ||
164 type.
id()==ID_c_enum_tag)
169 else if(type.
id()==ID_bool)
173 else if(type.
id()==ID_integer)
180 else if(expr.
id()==ID_array)
195 else if(expr.
id()==ID_struct)
197 std::string result=
"{ ";
208 else if(expr.
id()==ID_union)
221 const exprt &full_lhs,
230 std::string value_string;
233 value_string=
"(assignment removed)";
236 value_string=
from_expr(ns, identifier, value);
244 <<
"=" << value_string
259 out <<
"Initial State";
261 out <<
"State " << step_nr;
263 out <<
" " << source_location <<
" thread " << state.
thread_nr <<
"\n";
264 out <<
"----------------------------------------------------" 271 out <<
"----------------------------------------------------" 278 if(src.
id()==ID_index)
280 else if(src.
id()==ID_member)
282 else if(src.
id()==ID_symbol)
294 unsigned prev_step_nr=0;
295 bool first_step=
true;
296 std::size_t function_depth=0;
298 for(
const auto &step : goto_trace.
steps)
310 out <<
"Violated property:" <<
"\n";
311 if(!step.pc->source_location.is_nil())
312 out <<
" " << step.pc->source_location <<
"\n";
313 out <<
" " << step.comment <<
"\n";
315 if(step.pc->is_assert())
316 out <<
" " <<
from_expr(ns, step.pc->function, step.pc->guard)
327 out <<
"Violated assumption:" <<
"\n";
328 if(!step.pc->source_location.is_nil())
329 out <<
" " << step.pc->source_location <<
"\n";
331 if(step.pc->is_assume())
332 out <<
" " <<
from_expr(ns, step.pc->function, step.pc->guard)
346 if(step.pc->is_assign() ||
347 step.pc->is_return() ||
348 step.pc->is_function_call() ||
349 (step.pc->is_other() && step.lhs_object.is_not_nil()))
351 if(prev_step_nr!=step.step_nr || first_step)
354 prev_step_nr=step.step_nr;
356 out, ns, step, step.pc->source_location, step.step_nr, options);
374 step.lhs_object_value,
380 if(prev_step_nr!=step.step_nr || first_step)
383 prev_step_nr=step.step_nr;
385 out, ns, step, step.pc->source_location, step.step_nr, options);
389 out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value, options);
396 printf_formatter(
id2string(step.format_string), step.io_args);
397 printf_formatter.
print(out);
403 out, ns, step, step.pc->source_location, step.step_nr, options);
404 out <<
" OUTPUT " << step.io_id <<
":";
406 for(std::list<exprt>::const_iterator
407 l_it=step.io_args.begin();
408 l_it!=step.io_args.end();
411 if(l_it!=step.io_args.begin())
413 out <<
" " <<
from_expr(ns, step.pc->function, *l_it);
425 out, ns, step, step.pc->source_location, step.step_nr, options);
426 out <<
" INPUT " << step.io_id <<
":";
428 for(std::list<exprt>::const_iterator
429 l_it=step.io_args.begin();
430 l_it!=step.io_args.end();
433 if(l_it!=step.io_args.begin())
435 out <<
" " <<
from_expr(ns, step.pc->function, *l_it);
447 out <<
"\n#### Function call: " << step.identifier <<
" (depth " 448 << function_depth <<
") ####\n";
453 out <<
"\n#### Function return: " << step.identifier <<
" (depth " 454 << function_depth <<
") ####\n";
The type of an expression.
const std::string & id2string(const irep_idt &d)
void show_state_header(std::ostream &out, const namespacet &ns, const goto_trace_stept &state, const source_locationt &source_location, unsigned step_nr, const trace_optionst &options)
const std::string integer2string(const mp_integer &n, unsigned base)
std::string trace_numeric_value(const exprt &expr, const namespacet &ns, const trace_optionst &options)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static std::string numeric_representation(const exprt &expr, const trace_optionst &options)
Returns the numeric representation of an expression, based on options.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
unsignedbv_typet size_type()
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
goto_programt::const_targett pc
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)
void trace_value(std::ostream &out, const namespacet &ns, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &options)
#define PRECONDITION(CONDITION)
#define forall_operands(it, expr)
const typet & follow(const typet &) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool is_function_return() const
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Base class for all expressions.
irep_idt get_object_name() const
const std::string & get_string(const irep_namet &name) const
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
bool is_assignment() const
static const trace_optionst default_options
Expression providing an SSA-renamed symbol of expressions.