27 std::ostream &out)
const 29 for(
const auto &step :
steps)
35 std::ostream &out)
const 55 out <<
"FUNCTION RETURN";
break;
56 default: assert(
false);
67 if(!
pc->source_location.is_nil())
68 out <<
pc->source_location <<
"\n";
72 else if(
pc->is_assume())
74 else if(
pc->is_assert())
76 else if(
pc->is_dead())
78 else if(
pc->is_other())
80 else if(
pc->is_assign())
82 else if(
pc->is_decl())
84 else if(
pc->is_function_call())
91 if(
pc->is_other() ||
pc->is_assign())
98 else if(
pc->is_assert())
102 out <<
"Violated property:" <<
"\n";
103 if(
pc->source_location.is_nil())
104 out <<
" " <<
pc->source_location <<
"\n";
108 out <<
" " <<
from_expr(ns,
"",
pc->guard) <<
"\n";
122 if(expr.
id()==ID_constant)
124 if(type.
id()==ID_unsignedbv ||
125 type.
id()==ID_signedbv ||
127 type.
id()==ID_fixedbv ||
128 type.
id()==ID_floatbv ||
129 type.
id()==ID_pointer ||
130 type.
id()==ID_c_bit_field ||
131 type.
id()==ID_c_bool ||
132 type.
id()==ID_c_enum ||
133 type.
id()==ID_c_enum_tag)
137 else if(type.
id()==ID_bool)
142 else if(expr.
id()==ID_array)
157 else if(expr.
id()==ID_struct)
159 std::string result=
"{ ";
170 else if(expr.
id()==ID_union)
183 const exprt &full_lhs,
191 std::string value_string;
194 value_string=
"(assignment removed)";
197 value_string=
from_expr(ns, identifier, value);
205 <<
"=" << value_string
218 out <<
"Initial State";
220 out <<
"State " << step_nr;
222 out <<
" " << source_location
223 <<
" thread " << state.
thread_nr <<
"\n";
224 out <<
"----------------------------------------------------" <<
"\n";
229 if(src.
id()==ID_index)
231 else if(src.
id()==ID_member)
233 else if(src.
id()==ID_symbol)
244 unsigned prev_step_nr=0;
245 bool first_step=
true;
247 for(
const auto &step : goto_trace.
steps)
259 out <<
"Violated property:" <<
"\n";
260 if(!step.pc->source_location.is_nil())
261 out <<
" " << step.pc->source_location <<
"\n";
262 out <<
" " << step.comment <<
"\n";
264 if(step.pc->is_assert())
265 out <<
" " <<
from_expr(ns,
"", step.pc->guard) <<
"\n";
275 out <<
"Violated assumption:" <<
"\n";
276 if(!step.pc->source_location.is_nil())
277 out <<
" " << step.pc->source_location <<
"\n";
279 if(step.pc->is_assume())
280 out <<
" " <<
from_expr(ns,
"", step.pc->guard) <<
"\n";
293 if(step.pc->is_assign() ||
294 step.pc->is_return() ||
295 step.pc->is_function_call() ||
296 (step.pc->is_other() && step.lhs_object.is_not_nil()))
298 if(prev_step_nr!=step.step_nr || first_step)
301 prev_step_nr=step.step_nr;
308 out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
311 out, ns, step.lhs_object, step.lhs_object, step.lhs_object_value);
316 if(prev_step_nr!=step.step_nr || first_step)
319 prev_step_nr=step.step_nr;
323 trace_value(out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
330 printf_formatter(
id2string(step.format_string), step.io_args);
331 printf_formatter.
print(out);
337 out <<
" OUTPUT " << step.io_id <<
":";
339 for(std::list<exprt>::const_iterator
340 l_it=step.io_args.begin();
341 l_it!=step.io_args.end();
344 if(l_it!=step.io_args.begin())
358 out <<
" INPUT " << step.io_id <<
":";
360 for(std::list<exprt>::const_iterator
361 l_it=step.io_args.begin();
362 l_it!=step.io_args.end();
365 if(l_it!=step.io_args.begin())
The type of an expression.
const typet & follow(const typet &src) const
const std::string & id2string(const irep_idt &d)
std::string trace_value_binary(const exprt &expr, const namespacet &ns)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
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
const irep_idt & id() const
bool is_index_member_symbol(const exprt &src)
#define forall_operands(it, expr)
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 exprt & get_original_expr() const
const std::string & get_string(const irep_namet &name) const
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.