29 locs.
build(goto_functions);
68 statet &state=tmp_queue.front();
74 <<
", queue: " <<
queue.size()
76 for(
const auto &s :
queue)
77 debug() <<
' ' << s.get_depth();
106 status() <<
"Queue " << queue.size()
109 <<
" PC " << state.
pc()
133 queue.splice(queue.begin(), tmp_queue);
135 catch(
const std::string &e)
158 std::size_t number_of_visited_locations=0;
161 number_of_visited_locations++;
164 for(
unsigned l=0; l<loc_data.size(); l++)
165 if(!loc_data[l].visited)
170 status() <<
"Number of visited locations: " 171 << number_of_visited_locations <<
" (out of " 174 status() <<
"Number of dropped states: " 177 status() <<
"Number of paths: " 180 status() <<
"Number of infeasible paths: " 185 <<
" remaining after simplification" 189 status() <<
"Runtime: " << total_time <<
"s total, " 218 const goto_programt::instructiont &instruction=
223 if(instruction.source_location.is_not_nil())
226 if(instruction.source_location.get_comment()!=
"")
231 std::vector<path_symex_step_reft> steps;
234 for(
const auto &step_ref : steps)
236 if(step_ref->guard.is_not_nil())
238 std::string string_value=
from_expr(
ns,
"", step_ref->guard);
239 out <<
"{-" << count <<
"} " << string_value <<
'\n';
243 if(step_ref->ssa_rhs.is_not_nil())
245 equal_exprt equality(step_ref->ssa_lhs, step_ref->ssa_rhs);
246 std::string string_value=
from_expr(
ns,
"", equality);
247 out <<
"{-" << count <<
"} " << string_value <<
'\n';
252 out <<
"|--------------------------" <<
'\n';
254 exprt assertion=state.
read(instruction.guard);
256 out <<
"{" << 1 <<
"} " 272 if(!source_location.
is_nil() &&
276 <<
" line " << source_location.
get_line()
296 if(
unwind_limit!=std::numeric_limits<unsigned>::max() &&
297 pc->is_backwards_goto())
309 path_symex_statet::unwinding_mapt::const_iterator entry=
311 debug() << (stop?
"Not unwinding":
"Unwinding")
312 <<
" loop " <<
id <<
" iteration " 315 <<
" " << source_location
323 if(
unwind_limit!=std::numeric_limits<unsigned>::max() &&
324 pc->is_function_call())
336 const irep_idt id=
function.get(ID_identifier);
337 path_symex_statet::recursion_mapt::const_iterator entry=
340 debug() << (stop?
"Not unwinding":
"Unwinding")
341 <<
" recursion " <<
id <<
" iteration " 344 <<
" " << source_location
352 if(
time_limit!=std::numeric_limits<unsigned>::max() &&
356 if(pc->is_assume() &&
359 debug() <<
"aborting path on assume(false) at " 363 const irep_idt &c=pc->source_location.get_comment();
365 debug() <<
": " << c;
380 const goto_programt::instructiont &instruction=
383 irep_idt property_name=instruction.source_location.get_property_id();
393 state.
read(instruction.guard);
401 status() <<
"Checking property " << property_name <<
eom;
446 if(!it->second.is_inlined())
452 if(!i_it->is_assert())
std::size_t number_of_infeasible_paths
static irep_idt loop_id(const_targett target)
Human-readable loop name.
void build_history(std::vector< path_symex_step_reft > &dest) const
property_mapt property_map
exprt simplify_expr(const exprt &src, const namespacet &ns)
std::size_t number_of_locs
const irep_idt & get_function() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
virtual resultt operator()(const goto_functionst &goto_functions)
source_locationt source_location
std::size_t number_of_dropped_states
std::size_t number_of_paths
static mstreamt & eom(mstreamt &m)
void initialize_property_map(const goto_functionst &goto_functions)
unwinding_mapt unwinding_map
std::size_t number_of_feasible_paths
bool last_was_branch() const
bool drop_state(const statet &state)
decide whether to drop a state
instructionst::const_iterator const_targett
const irep_idt & get_line() const
exprt read(const exprt &src)
void path_symex(path_symex_statet &state, std::list< path_symex_statet > &further_states)
source_locationt last_source_location
source_locationt source_location
Build Goto Trace from Path Symex History.
std::size_t number_of_steps
bool is_feasible(class decision_proceduret &) const
unsigned long long get_t() const
virtual void set_message_handler(message_handlert &_message_handler)
bool is_feasible(statet &state)
unsigned get_current_thread() const
unsigned get_no_thread_interleavings() const
std::list< statet > queuet
std::size_t number_of_VCCs_after_simplification
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
std::size_t number_of_failed_properties
bool check_assertion(class decision_proceduret &)
const irep_idt & get_file() const
message_handlert & get_message_handler()
recursion_mapt recursion_map
absolute_timet current_time()
goto_programt::const_targett get_instruction() const
void do_show_vcc(statet &state)
Base class for all expressions.
bool is_executable() const
Path-based Symbolic Execution.
unsigned get_no_branches() const
Concrete Symbolic Transformer.
absolute_timet start_time
enum path_searcht::search_heuristict search_heuristic
const irep_idt & get_comment() const
void check_assertion(statet &state)
path_symex_statet initial_state(var_mapt &var_map, const locst &locs, path_symex_historyt &path_symex_history)
#define forall_goto_functions(it, functions)
const irep_idt & get_property_id() const
#define forall_goto_program_instructions(it, program)
path_symex_step_reft history
expanding_vectort< loc_datat > loc_data
std::size_t number_of_VCCs
unsigned get_depth() const
void build(const goto_functionst &goto_functions)
void build_goto_trace(const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator end_step, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
const code_function_callt & to_code_function_call(const codet &code)