26 bool is_backwards_goto)
36 const goto_programt::instructiont &instruction=*to;
37 for(
const auto &i_e : instruction.incoming_edges)
38 if(i_e->is_goto() && i_e->is_backwards_goto() &&
39 (!is_backwards_goto ||
40 state.
source.
pc->location_number>i_e->location_number))
54 const exprt &vcc_expr,
55 const std::string &msg,
82 exprt simplified_cond=cond;
91 exprt tmp=simplified_cond;
111 if(expr.
id()==ID_forall)
116 assert(expr.
op0().
id()==ID_symbol);
134 assert(!state.
threads.empty());
170 operator() (state, goto_functions, goto_program);
176 goto_functionst::function_mapt::const_iterator it=
180 throw "the program has no entry point";
193 std::cout <<
"\ninstruction type is " << state.
source.
pc->type <<
'\n';
194 std::cout <<
"Location: " << state.
source.
pc->source_location <<
'\n';
199 assert(!state.
threads.empty());
202 const goto_programt::instructiont &instruction=*state.
source.
pc;
209 if(max_depth!=0 && state.
depth>max_depth)
215 switch(instruction.type)
243 exprt tmp=instruction.guard;
258 exprt tmp(instruction.guard);
260 vcc(tmp, msg, state);
352 throw "symex got NO_INSTRUCTION";
355 throw "symex got unexpected instruction";
virtual void do_simplify(exprt &expr)
virtual void symex_atomic_begin(statet &state)
static irep_idt loop_id(const_targett target)
Human-readable loop name.
const std::string & id2string(const irep_idt &d)
virtual void location(const exprt &guard, const sourcet &source)=0
goto_programt::const_targett pc
virtual void symex_assume(statet &state, const exprt &cond)
void guard_expr(exprt &dest) const
void new_name(symbolt &symbol)
unsigned int get_unsigned_int_option(const std::string &option) const
Variables whose address is taken.
instructionst instructions
The list of instructions in the goto program.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
virtual void symex_decl(statet &state)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
symex_targett * symex_target
loop_iterationst loop_iterations
void return_assignment(statet &state)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
virtual void symex_step(const goto_functionst &goto_functions, statet &state)
execute just one step
void switch_to_thread(unsigned t)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
virtual void operator()(const goto_functionst &goto_functions)
symex all at once, starting from entry point
instructionst::const_iterator const_targett
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
#define Forall_expr(it, expr)
static irep_idt entry_point()
virtual void symex_transition(statet &state, goto_programt::const_targett to, bool is_backwards_goto=false)
API to expression classes.
virtual void symex_start_thread(statet &state)
virtual void symex_function_call(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)=0
virtual void symex_end_of_function(statet &state)
do function call by inlining
virtual void symex_other(const goto_functionst &goto_functions, statet &state)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void clean_expr(exprt &expr, statet &state, bool write)
function_mapt function_map
unsigned atomic_section_id
void merge_gotos(statet &state)
virtual void symex_dead(statet &state)
The boolean constant false.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)=0
void symex_assign_rec(statet &state, const code_assignt &code)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
symbol_tablet & new_symbol_table
virtual void symex_goto(statet &state)
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
call_stackt & call_stack()
virtual void symex_atomic_end(statet &state)
virtual void vcc(const exprt &expr, const std::string &msg, statet &state)
symex_targett::sourcet calling_location
Expression to hold a symbol (variable)
void symex_catch(statet &state)
void symex_throw(statet &state)
void rewrite_quantifiers(exprt &expr, statet &state)
void get_new_name(symbolt &symbol, const namespacet &ns)
automated variable renaming
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