12 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_H 13 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_H 158 bool is_backwards_goto=
false);
180 const std::string &msg,
189 const statet::goto_statet &goto_state,
193 const statet::goto_statet &goto_state,
197 const statet::goto_statet &goto_state,
236 const unsigned thread_nr,
270 const exprt &full_lhs,
277 const exprt &full_lhs,
284 const exprt &full_lhs,
291 const exprt &full_lhs,
298 const exprt &full_lhs,
305 const exprt &full_lhs,
312 const exprt &full_lhs,
341 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H virtual void do_simplify(exprt &expr)
goto_symext::statet & state
The type of an expression.
virtual void symex_atomic_begin(statet &state)
virtual void symex_step_goto(statet &state, bool taken)
irep_idt guard_identifier
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
virtual void symex_assign(statet &state, const code_assignt &code)
goto_programt::const_targett pc
virtual void symex_assume(statet &state, const exprt &cond)
void new_name(symbolt &symbol)
virtual void merge_goto(const statet::goto_statet &goto_state, statet &state)
void dereference_rec(exprt &expr, statet &state, guardt &guard, const bool write)
virtual void dereference(exprt &expr, statet &state, const bool write)
virtual void symex_function_call_symbol(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
virtual void symex_decl(statet &state)
void symex_assign_byte_extract(statet &state, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
Goto Programs with Functions.
static bool is_index_member_symbol_if(const exprt &expr)
virtual void symex_gcc_builtin_va_arg_next(statet &state, const exprt &lhs, const side_effect_exprt &code)
void symex_assign_if(statet &state, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
virtual void symex_trace(statet &state, const code_function_callt &code)
bool constant_propagation
exprt make_auto_object(const typet &type)
void process_array_expr_rec(exprt &expr, const typet &type) const
void replace_array_equal(exprt &expr)
The trinary if-then-else operator.
void parameter_assignments(const irep_idt function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments)
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
virtual void symex_macro(statet &state, const code_function_callt &code)
void locality(const irep_idt function_identifier, statet &state, const goto_functionst::goto_functiont &goto_function)
preserves locality of local variables of a given function by applying L1 renaming to the local identi...
void replace_nondet(exprt &expr)
Extract member of struct or union.
symex_targett::assignment_typet assignment_typet
void symex_assign_symbol(statet &state, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
static exprt add_to_lhs(const exprt &lhs, const exprt &what)
virtual void symex_printf(statet &state, const exprt &lhs, const exprt &rhs)
virtual void operator()(const goto_functionst &goto_functions)
symex all at once, starting from entry point
instructionst::const_iterator const_targett
Expression classes for byte-level operators.
static unsigned nondet_count
static unsigned dynamic_counter
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
void trigger_auto_object(const exprt &expr, statet &state)
virtual void symex_transition(statet &state, goto_programt::const_targett to, bool is_backwards_goto=false)
virtual void symex_start_thread(statet &state)
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
virtual void symex_function_call(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
virtual void symex_input(statet &state, const codet &code)
virtual void symex_end_of_function(statet &state)
do function call by inlining
virtual void symex_other(const goto_functionst &goto_functions, statet &state)
void clean_expr(exprt &expr, statet &state, bool write)
goto_function_templatet< goto_programt > goto_functiont
void symex_assign_struct_member(statet &state, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
void merge_gotos(statet &state)
virtual void symex_dead(statet &state)
virtual void symex_fkt(statet &state, const code_function_callt &code)
void dereference_rec_address_of(exprt &expr, statet &state, guardt &guard)
void initialize_auto_object(const exprt &expr, statet &state)
void symex_assign_rec(statet &state, const code_assignt &code)
void add_end_of_function(exprt &code, const irep_idt &identifier)
std::vector< exprt > operandst
virtual void symex_cpp_new(statet &state, const exprt &lhs, const side_effect_exprt &code)
unsigned atomic_section_counter
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
virtual void symex_transition(statet &state)
symbol_tablet & new_symbol_table
The main class for the forward symbolic simulator.
virtual void symex_function_call_code(const goto_functionst &goto_functions, statet &state, const code_function_callt &call)
do function call by inlining
virtual void symex_malloc(statet &state, const exprt &lhs, const side_effect_exprt &code)
virtual void symex_goto(statet &state)
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
Base class for all expressions.
virtual void symex_atomic_end(statet &state)
void phi_function(const statet::goto_statet &goto_state, statet &state)
virtual void vcc(const exprt &expr, const std::string &msg, statet &state)
void process_array_expr(exprt &expr)
virtual void loop_bound_exceeded(statet &state, const exprt &guard)
virtual void symex_cpp_delete(statet &state, const codet &code)
Expression to hold a symbol (variable)
void symex_catch(statet &state)
void set_option(const std::string &option, const bool value)
A statement in a programming language.
virtual void no_body(const irep_idt &identifier)
virtual void symex_output(statet &state, const codet &code)
An expression containing a side effect.
void symex_throw(statet &state)
void rewrite_quantifiers(exprt &expr, statet &state)
exprt address_arithmetic(const exprt &expr, statet &state, guardt &guard, bool keep_array)
Evaluate an ID_address_of expression.
goto_symext(const namespacet &_ns, symbol_tablet &_new_symbol_table, symex_targett &_target)
Expression providing an SSA-renamed symbol of expressions.
void symex_assign_typecast(statet &state, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
void pop_frame(statet &state)
pop one call frame
void symex_assign_array(statet &state, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &guard, assignment_typet assignment_type)
symex_targett::sourcet source