27 bool is_backwards_goto)
39 if(i_e->is_goto() && i_e->is_backwards_goto() &&
40 (!is_backwards_goto ||
41 state.
source.
pc->location_number>i_e->location_number))
49 const exprt &vcc_expr,
50 const std::string &msg,
77 exprt simplified_cond=cond;
86 exprt tmp=simplified_cond;
106 if(expr.
id()==ID_forall)
134 !pc->function.empty(),
"all symexed instructions should have a function");
136 pc->function, get_goto_function(pc->function));
154 std::cout <<
"********* Now executing thread " << t <<
'\n';
164 return [&goto_functions](
218 const statet &saved_state,
228 statet state(saved_state, saved_equation);
277 catch(
const std::out_of_range &error)
279 throw "the program has no entry point";
287 start_function->body.instructions.begin(),
288 prev(start_function->body.instructions.end()));
291 state, get_goto_function, new_symbol_table);
300 std::cout <<
"\ninstruction type is " << state.
source.
pc->type <<
'\n';
301 std::cout <<
"Location: " << state.
source.
pc->source_location <<
'\n';
320 switch(instruction.type)
348 exprt tmp=instruction.guard;
363 exprt tmp(instruction.guard);
365 vcc(tmp, msg, state);
457 throw "symex got NO_INSTRUCTION";
460 throw "symex got unexpected instruction";
virtual void symex_instruction_range(statet &, const goto_functionst &, goto_programt::const_targett first, goto_programt::const_targett limit)
Symexes from the first instruction and the given state, terminating as soon as the last instruction i...
void return_assignment(statet &)
const std::string & id2string(const irep_idt &d)
goto_programt::const_targett pc
void guard_expr(exprt &dest) const
virtual void symex_goto(statet &)
std::set< targett > incoming_edges
Variables whose address is taken.
virtual void symex_transition(statet &, goto_programt::const_targett to, bool is_backwards_goto=false)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
record an assumption
symex_target_equationt * symex_target
function_mapt function_map
loop_iterationst loop_iterations
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
virtual void do_simplify(exprt &)
void switch_to_thread(unsigned t)
#define INVARIANT(CONDITION, REASON)
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
virtual void symex_end_of_function(statet &)
do function call by inlining
unsigned depth
distance from entry
void symex_catch(statet &)
virtual void symex_atomic_end(statet &)
This class represents an instruction in the GOTO intermediate representation.
void symex_throw(statet &)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
virtual void symex_atomic_begin(statet &)
void initialize_entry_point(statet &state, const get_goto_functiont &get_goto_function, goto_programt::const_targett pc, goto_programt::const_targett limit)
Initialise the symbolic execution and the given state with pc as entry point.
virtual void symex_from_entry_point_of(const goto_functionst &goto_functions, symbol_tablet &new_symbol_table)
symex entire program starting from entry point
virtual void symex_other(statet &)
#define Forall_expr(it, expr)
static goto_symext::get_goto_functiont get_function_from_goto_functions(const goto_functionst &goto_functions)
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we're executing.
virtual void resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *const saved_equation, symbol_tablet &new_symbol_table)
Performs symbolic execution using a state and equation that have already been used to symex part of t...
virtual void symex_assume(statet &, const exprt &cond)
virtual void symex_decl(statet &)
API to expression classes.
symex_target_equationt & target
instructionst::const_iterator const_targett
::goto_functiont goto_functiont
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void populate_dirty_for_function(const irep_idt &id, const goto_functionst::goto_functiont &function)
Analyse the given function with dirtyt if it hasn't been seen before.
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
unsigned atomic_section_id
The boolean constant false.
void rewrite_quantifiers(exprt &, statet &)
void symex_assign(statet &, const code_assignt &)
virtual void vcc(const exprt &, const std::string &msg, statet &)
void symex_threaded_step(statet &, const get_goto_functiont &)
Invokes symex_step and verifies whether additional threads can be executed.
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
record an assertion
static irep_idt entry_point()
void clean_expr(exprt &, statet &, bool write)
bool should_pause_symex
Have states been pushed onto the workqueue?
Base class for all expressions.
call_stackt & call_stack()
virtual void symex_dead(statet &)
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc...
virtual void location(const exprt &guard, const sourcet &source)
just record a location
virtual void symex_start_thread(statet &)
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
void merge_gotos(statet &)
symex_targett::sourcet calling_location
Expression to hold a symbol (variable)
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
const bool doing_path_exploration
goto_programt::const_targett end_of_function
void add(const exprt &expr)
const code_function_callt & to_code_function_call(const codet &code)
symex_targett::sourcet source