24 record_coverage(false),
25 max_unwind_is_set(false),
40 <<
" line " << source_location.
get_line()
54 statistics() <<
"aborting path on assume(false) at " 69 (!cur_pc->is_end_function() ||
78 if(cur_pc->is_goto() &&
79 cur_pc->get_target()!=state.
source.
pc &&
80 cur_pc->guard.is_true())
96 assert(prev_pc->is_goto());
102 !prev_pc->guard.is_true())
115 unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
120 loop_limitst::const_iterator l_it=this_thread_limits.find(
id);
121 if(l_it!=this_thread_limits.end())
122 this_loop_limit=l_it->second;
127 this_loop_limit=l_it->second;
132 bool abort=unwind>=this_loop_limit;
134 statistics() << (abort?
"Not unwinding":
"Unwinding")
135 <<
" loop " <<
id <<
" iteration " 138 if(this_loop_limit!=std::numeric_limits<unsigned>::max())
139 statistics() <<
" (" << this_loop_limit <<
" max)";
141 statistics() <<
" " << source.pc->source_location
142 <<
" thread " << source.thread_nr << eom;
149 const unsigned thread_nr,
155 unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
160 loop_limitst::const_iterator l_it=this_thread_limits.find(
id);
161 if(l_it!=this_thread_limits.end())
162 this_loop_limit=l_it->second;
167 this_loop_limit=l_it->second;
172 bool abort=unwind>this_loop_limit;
174 if(unwind>0 || abort)
176 const symbolt &symbol=ns.lookup(
id);
178 statistics() << (abort?
"Not unwinding":
"Unwinding")
181 <<
" iteration " << unwind;
183 if(this_loop_limit!=std::numeric_limits<unsigned>::max())
184 statistics() <<
" (" << this_loop_limit <<
" max)";
197 "**** WARNING: no body for function " << identifier <<
eom;
static irep_idt loop_id(const_targett target)
Human-readable loop name.
goto_programt::const_targett pc
virtual void merge_goto(const statet::goto_statet &goto_state, statet &state)
exprt simplify_expr(const exprt &src, const namespacet &ns)
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
const irep_idt & get_function() const
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
virtual void symex_step(const goto_functionst &goto_functions, statet &state)
execute just one step
instructionst::const_iterator const_targett
const irep_idt & get_line() const
symex_coveraget symex_coverage
static irep_idt entry_point()
virtual void merge_goto(const statet::goto_statet &goto_state, statet &state)
void covered(goto_programt::const_targett from, goto_programt::const_targett to)
thread_loop_limitst thread_loop_limits
const irep_idt & display_name() const
The main class for the forward symbolic simulator.
const irep_idt & get_file() const
std::unordered_map< irep_idt, unsigned, irep_id_hash > loop_limitst
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
Bounded Model Checking for ANSI-C.
source_locationt last_source_location
std::unordered_set< irep_idt, irep_id_hash > body_warnings
virtual void symex_step(const goto_functionst &goto_functions, statet &state)
show progress
symex_bmct(const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target)
symex_targett::sourcet source
virtual void no_body(const irep_idt &identifier)
symex_targett::sourcet source