51 log.debug() <<
"BMC at " << source_location.
as_string() <<
" (depth "
64 log.statistics() <<
"aborting path on assume(false) at "
65 << state.
source.
pc->source_location() <<
" thread "
70 log.statistics() <<
": " << c;
72 log.statistics() <<
log.eom;
80 (!cur_pc->is_end_function() ||
90 cur_pc->is_goto() && cur_pc->get_target() != state.
source.
pc &&
91 cur_pc->condition().is_true())
104 const guardt prev_guard = goto_state.guard;
114 !prev_pc->condition().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())
156 log.statistics() <<
" (" << this_loop_limit <<
" max)";
158 log.statistics() <<
" " << source.
pc->source_location() <<
" thread "
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())
183 auto limit =
unwindset.get_limit(
id, thread_nr);
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())
203 log.statistics() <<
" (" << this_loop_limit <<
" max)";
205 log.statistics() <<
log.eom;
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
instructionst::const_iterator const_targett
Container for data that varies per program point, e.g.
unsigned depth
Distance from entry.
symex_targett::sourcet source
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
const symbol_table_baset & outer_symbol_table
The symbol table associated with the goto-program being executed.
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 ...
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...
guard_managert & guard_manager
Used to create guards.
goto_symext(message_handlert &mh, const symbol_table_baset &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager)
Construct a goto_symext to execute a particular program.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
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...
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.
messaget log
The messaget to write log messages to.
Storage for symbolic execution paths to be resumed later.
std::string as_string() const
const irep_idt & display_name() const
Return language specific display name if present.
symex_coveraget symex_coverage
bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind) override
std::vector< loop_unwind_handlert > loop_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
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...
source_locationt last_source_location
std::vector< recursion_unwind_handlert > recursion_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.
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, unwindsett &unwindset)
void symex_step(const get_goto_functiont &get_goto_function, statet &state) override
show progress
bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
Determine whether to unwind a loop.
const bool record_coverage
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
guard_expr_managert guard_managert
exprt simplify_expr(exprt src, const namespacet &ns)
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Identifies source in the context of symbolic execution.
goto_programt::const_targett pc
Bounded Model Checking for ANSI-C.