27 :
goto_symext(mh, outer_symbol_table, _target, options, path_storage),
28 record_coverage(false),
56 << state.
source.
pc->source_location <<
" thread " 70 (!cur_pc->is_end_function() ||
79 if(cur_pc->is_goto() &&
80 cur_pc->get_target()!=state.
source.
pc &&
81 cur_pc->guard.is_true())
103 !prev_pc->guard.is_true())
113 tvt abort_unwind_decision;
114 unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
118 abort_unwind_decision =
121 source.
pc->loop_number,
124 if(abort_unwind_decision.
is_known())
134 if(!limit.has_value())
135 abort_unwind_decision =
tvt(
false);
137 abort_unwind_decision =
tvt(unwind >= *limit);
141 abort_unwind_decision.
is_known(),
"unwind decision should be taken by now");
142 bool abort = abort_unwind_decision.
is_true();
144 log.
statistics() << (abort ?
"Not unwinding" :
"Unwinding") <<
" loop " <<
id 145 <<
" iteration " << unwind;
147 if(this_loop_limit!=std::numeric_limits<unsigned>::max())
158 const unsigned thread_nr,
161 tvt abort_unwind_decision;
162 unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
166 abort_unwind_decision = handler(
id, unwind, this_loop_limit);
167 if(abort_unwind_decision.
is_known())
177 if(!limit.has_value())
178 abort_unwind_decision =
tvt(
false);
180 abort_unwind_decision =
tvt(unwind > *limit);
184 abort_unwind_decision.
is_known(),
"unwind decision should be taken by now");
185 bool abort = abort_unwind_decision.
is_true();
187 if(unwind>0 || abort)
191 log.
statistics() << (abort ?
"Not unwinding" :
"Unwinding") <<
" recursion " 194 if(this_loop_limit!=std::numeric_limits<unsigned>::max())
207 log.
warning() <<
"**** WARNING: no body for function " << identifier
Generate Equation using Symbolic Execution.
goto_programt::const_targett pc
exprt simplify_expr(const exprt &src, const namespacet &ns)
std::unordered_set< irep_idt > body_warnings
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
std::string as_string() const
std::vector< recursion_unwind_handlert > recursion_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call. ...
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
static mstreamt & eom(mstreamt &m)
#define INVARIANT(CONDITION, REASON)
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
unsigned depth
distance from entry
mstreamt & warning() const
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
symex_coveraget symex_coverage
instructionst::const_iterator const_targett
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
#define PRECONDITION(CONDITION)
virtual void merge_goto(const statet::goto_statet &goto_state, statet &state)
void covered(goto_programt::const_targett from, goto_programt::const_targett to)
Storage for symbolic execution paths to be resumed later.
const irep_idt & display_name() const
The main class for the forward symbolic simulator.
static irep_idt entry_point()
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
symex_bmct(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage)
Bounded Model Checking for ANSI-C.
virtual void symex_step(const get_goto_functiont &get_goto_function, statet &state)
show progress
source_locationt last_source_location
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
std::vector< loop_unwind_handlert > loop_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
symex_targett::sourcet source
mstreamt & statistics() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
virtual void no_body(const irep_idt &identifier)
symex_targett::sourcet source