Go to the documentation of this file.
35 record_coverage(!options.get_option(
"symex-coverage-report").empty()),
36 havoc_bodyless_functions(
37 options.get_bool_option(
"havoc-undefined-functions")),
65 << state.
source.
pc->source_location <<
" thread "
80 (!cur_pc->is_end_function() ||
90 cur_pc->is_goto() && cur_pc->get_target() != state.
source.
pc &&
91 cur_pc->guard.is_true())
104 const guardt prev_guard = goto_state.guard;
114 !prev_pc->guard.is_true())
125 tvt abort_unwind_decision;
126 unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
130 abort_unwind_decision =
131 handler(context, source.
pc->loop_number, unwind, this_loop_limit);
132 if(abort_unwind_decision.
is_known())
142 if(!limit.has_value())
143 abort_unwind_decision =
tvt(
false);
145 abort_unwind_decision =
tvt(unwind >= *limit);
149 abort_unwind_decision.
is_known(),
"unwind decision should be taken by now");
150 bool abort = abort_unwind_decision.
is_true();
152 log.
statistics() << (abort ?
"Not unwinding" :
"Unwinding") <<
" loop " <<
id
153 <<
" iteration " << unwind;
155 if(this_loop_limit != std::numeric_limits<unsigned>::max())
169 tvt abort_unwind_decision;
170 unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
174 abort_unwind_decision = handler(
id, unwind, this_loop_limit);
175 if(abort_unwind_decision.
is_known())
185 if(!limit.has_value())
186 abort_unwind_decision =
tvt(
false);
188 abort_unwind_decision =
tvt(unwind > *limit);
192 abort_unwind_decision.
is_known(),
"unwind decision should be taken by now");
193 bool abort = abort_unwind_decision.
is_true();
195 if(unwind > 0 || abort)
199 log.
statistics() << (abort ?
"Not unwinding" :
"Unwinding") <<
" recursion "
202 if(this_loop_limit != std::numeric_limits<unsigned>::max())
215 log.
warning() <<
"**** WARNING: no body for function " << identifier;
220 <<
"; assigning non-deterministic values to any pointer arguments";
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Generate Equation using Symbolic Execution.
virtual void symex_step(const get_goto_functiont &get_goto_function, statet &state)
Called for each step in the symbolic execution This calls print_symex_step to print symex's current i...
std::string as_string() const
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.
Central data structure: state.
const bool record_coverage
symex_targett::sourcet source
std::unordered_set< irep_idt > body_warnings
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.
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
messaget log
The messaget to write log messages to.
This is unused by this implementation of guards, but can be used by other implementations of the same...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
virtual void merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state)
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall sy...
symex_bmct(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager)
unsigned depth
Distance from entry.
#define PRECONDITION(CONDITION)
The main class for the forward symbolic simulator.
void covered(goto_programt::const_targett from, goto_programt::const_targett to)
exprt simplify_expr(exprt src, const namespacet &ns)
symex_coveraget symex_coverage
bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
Determine whether to unwind a loop.
Container for data that varies per program point, e.g.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
const bool havoc_bodyless_functions
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
void symex_step(const get_goto_functiont &get_goto_function, statet &state) override
show progress
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind) override
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
void merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state) override
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall sy...
instructionst::const_iterator const_targett
Identifies source in the context of symbolic execution.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
mstreamt & warning() const
void no_body(const irep_idt &identifier) override
Log a warning that a function has no body.
source_locationt last_source_location
Bounded Model Checking for ANSI-C.
mstreamt & statistics() const