12 #ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_H 13 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_H 62 options.get_bool_option(
"allow-pointer-unsoundness")),
83 std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
112 const statet &saved_state,
285 bool is_backwards_goto=
false);
305 const std::string &msg,
314 const statet::goto_statet &goto_state,
318 const statet::goto_statet &goto_state,
322 const statet::goto_statet &goto_state,
361 const unsigned thread_nr,
397 const exprt &full_lhs,
404 const exprt &full_lhs,
411 const exprt &full_lhs,
418 const exprt &full_lhs,
425 const exprt &full_lhs,
432 const exprt &full_lhs,
439 const exprt &full_lhs,
470 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H goto_symext::statet & state
The type of an expression.
virtual void symex_gcc_builtin_va_arg_next(statet &, const exprt &lhs, const side_effect_exprt &)
const bool allow_pointer_unsoundness
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 &)
irep_idt guard_identifier
Generate Equation using Symbolic Execution.
virtual bool get_unwind_recursion(const irep_idt &identifier, const unsigned thread_nr, unsigned unwind)
goto_programt::const_targett pc
virtual void symex_goto(statet &)
virtual void symex_fkt(statet &, const code_function_callt &)
virtual void symex_transition(statet &, goto_programt::const_targett to, bool is_backwards_goto=false)
void replace_nondet(exprt &)
Goto Programs with Functions.
static bool is_index_member_symbol_if(const exprt &expr)
bool constant_propagation
void symex_assign_byte_extract(statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void merge_goto(const statet::goto_statet &goto_state, statet &)
virtual void symex_step_goto(statet &, bool taken)
The trinary if-then-else operator.
virtual void symex_macro(statet &, const code_function_callt &)
virtual void symex_function_call_symbol(const get_goto_functiont &, statet &, const code_function_callt &)
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
virtual void do_simplify(exprt &)
goto_symext(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage)
void symex_assign_rec(statet &, const exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void symex_step(const get_goto_functiont &, statet &)
do just one step
Extract member of struct or union.
virtual void symex_end_of_function(statet &)
do function call by inlining
void symex_catch(statet &)
virtual void symex_atomic_end(statet &)
virtual void dereference(exprt &, statet &, const bool write)
symex_targett::assignment_typet assignment_typet
void symex_throw(statet &)
static exprt add_to_lhs(const exprt &lhs, const exprt &what)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
bool self_loops_to_assumptions
virtual void symex_atomic_begin(statet &)
void symex_assign_typecast(statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void symex_allocate(statet &, const exprt &lhs, const side_effect_exprt &)
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.
static unsigned nondet_count
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 &)
virtual void symex_cpp_new(statet &, const exprt &lhs, const side_effect_exprt &)
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes...
virtual void symex_with_state(statet &, const goto_functionst &, symbol_tablet &)
symex entire program starting from entry point
static unsigned dynamic_counter
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program that we're executing.
virtual bool get_unwind(const symex_targett::sourcet &source, unsigned unwind)
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...
exprt address_arithmetic(const exprt &, statet &, guardt &, bool keep_array)
Evaluate an ID_address_of expression.
virtual void symex_assume(statet &, const exprt &cond)
virtual void symex_decl(statet &)
symex_target_equationt & target
void merge_value_sets(const statet::goto_statet &goto_state, statet &dest)
instructionst::const_iterator const_targett
::goto_functiont goto_functiont
path_storaget & path_storage
void locality(const irep_idt function_identifier, statet &, const goto_functionst::goto_functiont &)
preserves locality of local variables of a given function by applying L1 renaming to the local identi...
void dereference_rec(exprt &, statet &, guardt &, const bool write)
exprt make_auto_object(const typet &, statet &)
virtual void symex_trace(statet &, const code_function_callt &)
virtual void loop_bound_exceeded(statet &, const exprt &guard)
void pop_frame(statet &)
pop one call frame
void symex_assign_if(statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
Storage for symbolic execution paths to be resumed later.
void add_end_of_function(exprt &code, const irep_idt &identifier)
std::vector< exprt > operandst
void parameter_assignments(const irep_idt function_identifier, const goto_functionst::goto_functiont &, statet &, const exprt::operandst &arguments)
unsigned atomic_section_counter
virtual void symex_input(statet &, const codet &)
void phi_function(const statet::goto_statet &goto_state, statet &)
virtual void symex_transition(statet &state)
void rewrite_quantifiers(exprt &, statet &)
void symex_assign(statet &, const code_assignt &)
virtual void vcc(const exprt &, const std::string &msg, statet &)
The main class for the forward symbolic simulator.
void symex_threaded_step(statet &, const get_goto_functiont &)
Invokes symex_step and verifies whether additional threads can be executed.
void process_array_expr(exprt &)
Given an expression, find the root object and the offset into it.
void clean_expr(exprt &, statet &, bool write)
Expression to hold a nondeterministic choice.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use...
void dereference_rec_address_of(exprt &, statet &, guardt &)
bool should_pause_symex
Have states been pushed onto the workqueue?
Base class for all expressions.
virtual void symex_function_call_code(const get_goto_functiont &, statet &, const code_function_callt &)
do function call by inlining
void trigger_auto_object(const exprt &, statet &)
virtual void symex_output(statet &, const codet &)
void symex_assign_struct_member(statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
void initialize_auto_object(const exprt &, statet &)
virtual void symex_dead(statet &)
virtual void symex_start_thread(statet &)
void merge_gotos(statet &)
Expression to hold a symbol (variable)
void symex_assign_array(statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)
virtual void symex_printf(statet &, const exprt &lhs, const exprt &rhs)
A statement in a programming language.
virtual void no_body(const irep_idt &identifier)
An expression containing a side effect.
virtual void symex_function_call(const get_goto_functiont &, statet &, const code_function_callt &)
const bool doing_path_exploration
virtual void symex_cpp_delete(statet &, const codet &)
Expression providing an SSA-renamed symbol of expressions.
Storage of symbolic execution paths to resume.
nondet_symbol_exprt build_symex_nondet(typet &type)
void havoc_rec(statet &, const guardt &, const exprt &)
symex_targett::sourcet source
void symex_assign_symbol(statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, guardt &, assignment_typet)