30 incr_loop_id(options.get_option(
"incremental-loop")),
32 options.is_set(
"unwind-max") ? options.get_signed_int_option(
"unwind-max")
33 : std::numeric_limits<unsigned>::max()),
35 options.is_set(
"unwind-min") ? options.get_signed_int_option(
"unwind-min")
55 tvt abort_unwind_decision;
56 unsigned this_loop_limit = std::numeric_limits<unsigned>::max();
65 abort_unwind_decision =
tvt(unwind >= this_loop_limit);
71 abort_unwind_decision =
72 handler(context, source.
pc->loop_number, unwind, this_loop_limit);
83 if(!limit.has_value())
84 abort_unwind_decision =
tvt(
false);
86 abort_unwind_decision =
tvt(unwind >= *limit);
91 abort_unwind_decision.
is_known(),
"unwind decision should be taken by now");
92 bool abort = abort_unwind_decision.
is_true();
95 log.
statistics() << (abort ?
"Not unwinding" :
"Unwinding") <<
" loop " <<
id
96 <<
" iteration " << unwind;
98 if(this_loop_limit != std::numeric_limits<unsigned>::max())
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
bool ignore_assertions
If this flag is set to true then assertions will be temporarily ignored by the symbolic executions.
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 ...
std::unique_ptr< statet > initialize_entry_point_state(const get_goto_functiont &get_goto_function)
Initialize the symbolic execution and the given state with the beginning of the entry point function.
virtual void symex_with_state(statet &state, const get_goto_functiont &get_goto_functions, symbol_tablet &new_symbol_table)
Symbolically execute the entire program starting from entry point.
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.
bool should_pause_symex
Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution ...
mstreamt & statistics() const
bool get_bool_option(const std::string &option) const
Storage for symbolic execution paths to be resumed later.
A way of representing nested key/value data.
const unsigned incr_min_unwind
bool resume(const get_goto_functiont &get_goto_function)
Return true if symex can be resumed.
bool from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
Return true if symex can be resumed.
const unsigned incr_max_unwind
const irep_idt incr_loop_id
void log_unwinding(unsigned unwind)
bool check_break(const irep_idt &loop_id, unsigned unwind) override
Defines condition for interrupting symbolic execution for incremental BMC.
std::unique_ptr< goto_symext::statet > state
symex_bmc_incremental_one_loopt(message_handlert &, const symbol_tablet &outer_symbol_table, symex_target_equationt &, const optionst &, path_storaget &, guard_managert &, ui_message_handlert::uit output_ui)
bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
Determine whether to unwind a loop.
std::vector< loop_unwind_handlert > loop_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
This is unused by this implementation of guards, but can be used by other implementations of the same...
static structured_data_entryt data_node(const jsont &data)
Identifies source in the context of symbolic execution.
goto_programt::const_targett pc