Go to the documentation of this file.
27 :
goto_symext(mh, outer_symbol_table, _target, options, path_storage),
28 record_coverage(!options.get_option(
"symex-coverage-report").empty()),
56 << state.
source.
pc->source_location <<
" thread "
71 (!cur_pc->is_end_function() ||
80 if(cur_pc->is_goto() &&
81 cur_pc->get_target()!=state.
source.
pc &&
82 cur_pc->guard.is_true())
104 !prev_pc->guard.is_true())
115 tvt abort_unwind_decision;
116 unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
120 abort_unwind_decision =
121 handler(context, source.
pc->loop_number, unwind, this_loop_limit);
122 if(abort_unwind_decision.
is_known())
132 if(!limit.has_value())
133 abort_unwind_decision =
tvt(
false);
135 abort_unwind_decision =
tvt(unwind >= *limit);
139 abort_unwind_decision.
is_known(),
"unwind decision should be taken by now");
140 bool abort = abort_unwind_decision.
is_true();
142 log.
statistics() << (abort ?
"Not unwinding" :
"Unwinding") <<
" loop " <<
id
143 <<
" iteration " << unwind;
145 if(this_loop_limit!=std::numeric_limits<unsigned>::max())
156 const unsigned thread_nr,
159 tvt abort_unwind_decision;
160 unsigned this_loop_limit=std::numeric_limits<unsigned>::max();
164 abort_unwind_decision = handler(
id, unwind, this_loop_limit);
165 if(abort_unwind_decision.
is_known())
175 if(!limit.has_value())
176 abort_unwind_decision =
tvt(
false);
178 abort_unwind_decision =
tvt(unwind > *limit);
182 abort_unwind_decision.
is_known(),
"unwind decision should be taken by now");
183 bool abort = abort_unwind_decision.
is_true();
185 if(unwind>0 || abort)
189 log.
statistics() << (abort ?
"Not unwinding" :
"Unwinding") <<
" recursion "
192 if(this_loop_limit!=std::numeric_limits<unsigned>::max())
205 log.
warning() <<
"**** WARNING: no body for function " << identifier
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
std::string as_string() const
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
std::vector< loop_unwind_handlert > loop_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
const irep_idt & display_name() const
Return language specific display name if present.
goto_programt::const_targett pc
Storage for symbolic execution paths to be resumed later.
void merge_goto(const statet::goto_statet &goto_state, statet &state) override
const bool record_coverage
symex_targett::sourcet source
std::unordered_set< irep_idt > body_warnings
exprt simplify_expr(const exprt &src, const namespacet &ns)
bool is_false() const
Return whether the expression is a constant representing false.
std::vector< recursion_unwind_handlert > recursion_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.
bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind) override
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
unsigned depth
distance from entry
The main class for the forward symbolic simulator.
void covered(goto_programt::const_targett from, goto_programt::const_targett to)
bool should_stop_unwind(const symex_targett::sourcet &source, const goto_symex_statet::call_stackt &context, unsigned unwind) override
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
symex_coveraget symex_coverage
std::vector< framet > call_stackt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
symex_targett::sourcet source
void symex_step(const get_goto_functiont &get_goto_function, statet &state) override
show progress
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
instructionst::const_iterator const_targett
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
Identifies source in the context of symbolic execution.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symex_bmct(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage)
mstreamt & warning() const
void no_body(const irep_idt &identifier) override
source_locationt last_source_location
mstreamt & statistics() const