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';
113 if(expr.
id()==ID_constant)
115 if(type.
id()==ID_unsignedbv ||
116 type.
id()==ID_signedbv ||
118 type.
id()==ID_fixedbv ||
119 type.
id()==ID_floatbv ||
120 type.
id()==ID_pointer ||
121 type.
id()==ID_c_bit_field ||
122 type.
id()==ID_c_bool ||
123 type.
id()==ID_c_enum ||
124 type.
id()==ID_c_enum_tag)
126 const std::string & str = expr.
get_string(ID_value);
128 std::ostringstream oss;
130 for(
const auto c : str)
133 if(++i % 8 == 0 && str.size() != i)
139 else if(type.
id()==ID_bool)
143 else if(type.
id()==ID_integer)
150 else if(expr.
id()==ID_array)
165 else if(expr.
id()==ID_struct)
167 std::string result=
"{ ";
178 else if(expr.
id()==ID_union)
191 const exprt &full_lhs,
199 std::string value_string;
202 value_string=
"(assignment removed)";
205 value_string=
from_expr(ns, identifier, value);
213 <<
"=" << value_string
226 out <<
"Initial State";
228 out <<
"State " << step_nr;
230 out <<
" " << source_location
231 <<
" thread " << state.
thread_nr <<
"\n";
232 out <<
"----------------------------------------------------" <<
"\n";
237 if(src.
id()==ID_index)
239 else if(src.
id()==ID_member)
241 else if(src.
id()==ID_symbol)
252 unsigned prev_step_nr=0;
253 bool first_step=
true;
255 for(
const auto &step : goto_trace.
steps)
267 out <<
"Violated property:" <<
"\n";
268 if(!step.pc->source_location.is_nil())
269 out <<
" " << step.pc->source_location <<
"\n";
270 out <<
" " << step.comment <<
"\n";
272 if(step.pc->is_assert())
273 out <<
" " <<
from_expr(ns, step.pc->function, step.pc->guard)
284 out <<
"Violated assumption:" <<
"\n";
285 if(!step.pc->source_location.is_nil())
286 out <<
" " << step.pc->source_location <<
"\n";
288 if(step.pc->is_assume())
289 out <<
" " <<
from_expr(ns, step.pc->function, step.pc->guard)
303 if(step.pc->is_assign() ||
304 step.pc->is_return() ||
305 step.pc->is_function_call() ||
306 (step.pc->is_other() && step.lhs_object.is_not_nil()))
308 if(prev_step_nr!=step.step_nr || first_step)
311 prev_step_nr=step.step_nr;
318 out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
321 out, ns, step.lhs_object, step.lhs_object, step.lhs_object_value);
326 if(prev_step_nr!=step.step_nr || first_step)
329 prev_step_nr=step.step_nr;
333 trace_value(out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
340 printf_formatter(
id2string(step.format_string), step.io_args);
341 printf_formatter.
print(out);
347 out <<
" OUTPUT " << step.io_id <<
":";
349 for(std::list<exprt>::const_iterator
350 l_it=step.io_args.begin();
351 l_it!=step.io_args.end();
354 if(l_it!=step.io_args.begin())
356 out <<
" " <<
from_expr(ns, step.pc->function, *l_it);
368 out <<
" INPUT " << step.io_id <<
":";
370 for(std::list<exprt>::const_iterator
371 l_it=step.io_args.begin();
372 l_it!=step.io_args.end();
375 if(l_it!=step.io_args.begin())
377 out <<
" " <<
from_expr(ns, step.pc->function, *l_it);
The type of an expression.
const std::string & id2string(const irep_idt &d)
std::string trace_value_binary(const exprt &expr, const namespacet &ns)
const std::string integer2string(const mp_integer &n, unsigned base)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
unsignedbv_typet size_type()
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
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)
#define forall_operands(it, expr)
const typet & follow(const typet &) const
bool is_function_return() const
void trace_value(std::ostream &out, const namespacet &ns, const ssa_exprt &lhs_object, const exprt &full_lhs, const exprt &value)
Base class for all expressions.
irep_idt get_object_name() const
const std::string & get_string(const irep_namet &name) const
bool is_assignment() const
static const trace_optionst default_options
void show_state_header(std::ostream &out, const goto_trace_stept &state, const source_locationt &source_location, unsigned step_nr)
Expression providing an SSA-renamed symbol of expressions.