|
typedef goto_symex_statet | statet |
| A type abbreviation for goto_symex_statet.
|
typedef std::function< const goto_functionst::goto_functiont &(const irep_idt &)> | get_goto_functiont |
| The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
|
static get_goto_functiont | get_goto_function (abstract_goto_modelt &goto_model) |
| Return a function to get/load a goto function from the given goto model Create a default delegate to retrieve function bodies from a goto_functionst.
|
bool | should_pause_symex |
| Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution run, it means that symbolic execution has been paused because we encountered a GOTO instruction while doing path exploration, and thus pushed the successor states of the GOTO onto path_storage.
|
bool | ignore_assertions = false |
| If this flag is set to true then assertions will be temporarily ignored by the symbolic executions.
|
irep_idt | language_mode |
| language_mode: ID_java, ID_C or another language identifier if we know the source language in use, irep_idt() otherwise.
|
typedef symex_targett::assignment_typet | assignment_typet |
std::unique_ptr< statet > | initialize_entry_point_state (const get_goto_functiont &get_goto_function) |
| Initialize the symbolic execution and the given state with the beginning of the entry point function.
|
void | symex_threaded_step (statet &state, const get_goto_functiont &get_goto_function) |
| Invokes symex_step and verifies whether additional threads can be executed.
|
virtual void | symex_step (const get_goto_functiont &get_goto_function, statet &state) |
| Called for each step in the symbolic execution This calls print_symex_step to print symex's current instruction if required, then execute_next_instruction to execute the actual instruction body.
|
void | execute_next_instruction (const get_goto_functiont &get_goto_function, statet &state) |
| Executes the instruction state.source.pc Case-switches over the type of the instruction being executed and calls another function appropriate to the instruction type, for example symex_function_call if the current instruction is a function call, symex_goto if the current instruction is a goto, etc.
|
void | kill_instruction_local_symbols (statet &state) |
| Kills any variables in instruction_local_symbols (these are currently always let-bound variables defined in the course of executing the current instruction), then clears instruction_local_symbols.
|
void | print_symex_step (statet &state) |
| Prints the route of symex as it walks through the code.
|
messaget::mstreamt & | print_callstack_entry (const symex_targett::sourcet &target) |
exprt | clean_expr (exprt expr, statet &state, bool write) |
| Clean up an expression.
|
void | trigger_auto_object (const exprt &, statet &) |
void | initialize_auto_object (const exprt &, statet &) |
void | process_array_expr (statet &, exprt &) |
| Given an expression, find the root object and the offset into it.
|
exprt | make_auto_object (const typet &, statet &) |
virtual void | dereference (exprt &, statet &, bool write) |
| Replace all dereference operations within expr with explicit references to the objects they may refer to. For example, the expression *p1 + *p2 might be rewritten to obj1 + (p2 == &obj2 ? obj2 : obj3) in the case where p1 is known to point to obj1 and p2 points to either obj2 or obj3. The expression, and any object references introduced, are renamed to L1 in the process (so in fact we would get obj1!0@3 + (p2!0@1 == .... rather than the exact example given above).
|
symbol_exprt | cache_dereference (exprt &dereference_result, statet &state) |
void | dereference_rec (exprt &expr, statet &state, bool write, bool is_in_quantifier) |
exprt | address_arithmetic (const exprt &, statet &, bool keep_array) |
virtual void | symex_goto (statet &state) |
| Symbolically execute a GOTO instruction.
|
void | symex_unreachable_goto (statet &state) |
| Symbolically execute a GOTO instruction in the context of unreachable code.
|
void | symex_set_return_value (statet &state, const exprt &return_value) |
| Symbolically execute a SET_RETURN_VALUE instruction.
|
virtual void | symex_start_thread (statet &state) |
| Symbolically execute a START_THREAD instruction.
|
virtual void | symex_atomic_begin (statet &state) |
| Symbolically execute an ATOMIC_BEGIN instruction.
|
virtual void | symex_atomic_end (statet &state) |
| Symbolically execute an ATOMIC_END instruction.
|
virtual void | symex_decl (statet &state) |
| Symbolically execute a DECL instruction.
|
virtual void | symex_decl (statet &state, const symbol_exprt &expr) |
| Symbolically execute a DECL instruction for the given symbol or simulate such an execution for a synthetic symbol.
|
virtual void | symex_dead (statet &state) |
| Symbolically execute a DEAD instruction.
|
void | symex_dead (statet &state, const symbol_exprt &symbol_expr) |
| Kill a symbol, as if it had been the subject of a DEAD instruction.
|
virtual void | symex_other (statet &state) |
| Symbolically execute an OTHER instruction.
|
void | symex_assert (const goto_programt::instructiont &, statet &) |
void | apply_goto_condition (goto_symex_statet ¤t_state, goto_statet &jump_taken_state, goto_statet &jump_not_taken_state, const exprt &original_guard, const exprt &new_guard, const namespacet &ns) |
| Propagate constants and points-to information implied by a GOTO condition.
|
void | try_filter_value_sets (goto_symex_statet &state, exprt condition, const value_sett &original_value_set, value_sett *jump_taken_value_set, value_sett *jump_not_taken_value_set, const namespacet &ns) |
| Try to filter value sets based on whether possible values of a pointer-typed symbol make the condition true or false.
|
virtual void | vcc (const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state) |
| Symbolically execute a verification condition (assertion).
|
virtual void | symex_assume (statet &state, const exprt &cond) |
| Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption.
|
void | symex_assume_l2 (statet &, const exprt &cond) |
void | merge_gotos (statet &state) |
| Merge all branches joining at the current program point.
|
virtual void | merge_goto (const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state) |
| Merge a single branch, the symbolic state of which is held in goto_state , into the current overall symbolic state.
|
void | phi_function (const goto_statet &goto_state, statet &dest_state) |
| Merge the SSA assignments from goto_state into dest_state.
|
virtual bool | should_stop_unwind (const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) |
| Determine whether to unwind a loop.
|
virtual void | loop_bound_exceeded (statet &state, const exprt &guard) |
virtual void | symex_function_call (const get_goto_functiont &get_goto_function, statet &state, const goto_programt::instructiont &instruction) |
| Symbolically execute a FUNCTION_CALL instruction.
|
virtual void | locality (const irep_idt &function_identifier, goto_symext::statet &state, const goto_functionst::goto_functiont &goto_function) |
| Preserves locality of parameters of a given function by applying L1 renaming to them.
|
virtual void | symex_end_of_function (statet &) |
| Symbolically execute a END_FUNCTION instruction.
|
virtual void | symex_function_call_symbol (const get_goto_functiont &get_goto_function, statet &state, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments) |
| Symbolic execution of a call to a function call.
|
virtual void | symex_function_call_post_clean (const get_goto_functiont &get_goto_function, statet &state, const exprt &cleaned_lhs, const symbol_exprt &function, const exprt::operandst &cleaned_arguments) |
| Symbolic execution of a function call by inlining.
|
virtual bool | get_unwind_recursion (const irep_idt &identifier, unsigned thread_nr, unsigned unwind) |
void | parameter_assignments (const irep_idt &function_identifier, const goto_functionst::goto_functiont &goto_function, statet &state, const exprt::operandst &arguments) |
| Iterates over arguments and assigns them to the parameters, which are symbols whose name and type are deduced from the type of goto_function .
|
void | symex_throw (statet &state) |
| Symbolically execute a THROW instruction.
|
void | symex_catch (statet &state) |
| Symbolically execute a CATCH instruction.
|
virtual void | do_simplify (exprt &expr, const value_sett &value_set) |
void | symex_assign (statet &state, const exprt &lhs, const exprt &rhs) |
| Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
|
bool | constant_propagate_assignment_with_side_effects (statet &state, symex_assignt &symex_assign, const exprt &lhs, const exprt &rhs) |
| Attempt to constant propagate side effects of the assignment (if any)
|
void | constant_propagate_empty_string (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Create an empty string constant.
|
bool | constant_propagate_string_concat (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Attempt to constant propagate string concatenation.
|
bool | constant_propagate_string_substring (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Attempt to constant propagate getting a substring of a string.
|
bool | constant_propagate_integer_to_string (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Attempt to constant propagate converting an integer to a string.
|
bool | constant_propagate_delete_char_at (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Attempt to constant propagate deleting a character from a string.
|
bool | constant_propagate_delete (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Attempt to constant propagate deleting a substring from a string.
|
bool | constant_propagate_set_length (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Attempt to constant propagate setting the length of a string.
|
bool | constant_propagate_set_char_at (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Attempt to constant propagate setting the char at the given index.
|
bool | constant_propagate_trim (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Attempt to constant propagate trim operations.
|
bool | constant_propagate_case_change (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1, bool to_upper) |
| Attempt to constant propagate case changes, both upper and lower.
|
bool | constant_propagate_replace (statet &state, symex_assignt &symex_assign, const function_application_exprt &f_l1) |
| Attempt to constant proagate character replacement.
|
void | assign_string_constant (statet &state, symex_assignt &symex_assign, const ssa_exprt &length, const constant_exprt &new_length, const ssa_exprt &char_array, const array_exprt &new_char_array) |
| Assign constant string length and string data given by a char array to given ssa variables.
|
const symbolt & | get_new_string_data_symbol (statet &state, symex_assignt &symex_assign, const std::string &aux_symbol_name, const ssa_exprt &char_array, const array_exprt &new_char_array) |
| Installs a new symbol in the symbol table to represent the given character array, and assigns the character array to the symbol.
|
void | associate_array_to_pointer (statet &state, symex_assignt &symex_assign, const array_exprt &new_char_array, const address_of_exprt &string_data) |
| Generate array to pointer association primitive.
|
std::optional< std::reference_wrapper< const array_exprt > > | try_evaluate_constant_string (const statet &state, const exprt &content) |
void | havoc_rec (statet &state, const guardt &guard, const exprt &dest) |
static std::optional< std::reference_wrapper< const constant_exprt > > | try_evaluate_constant (const statet &state, const exprt &expr) |
const symex_configt | symex_config |
| The configuration to use for this symbolic execution.
|
const symbol_table_baset & | outer_symbol_table |
| The symbol table associated with the goto-program being executed.
|
namespacet | ns |
| Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol table owned by the goto_symex_statet object used during symbolic execution.
|
guard_managert & | guard_manager |
| Used to create guards.
|
symex_target_equationt & | target |
| The equation that this execution is building up.
|
unsigned | atomic_section_counter |
| A monotonically increasing index for each encountered ATOMIC_BEGIN instruction.
|
std::vector< symbol_exprt > | instruction_local_symbols |
| Variables that should be killed at the end of the current symex_step invocation.
|
messaget | log |
| The messaget to write log messages to.
|
std::size_t | path_segment_vccs |
| Execute any let expressions in expr using symex_assignt::assign_symbol.
|
complexity_limitert | complexity_module |
shadow_memoryt | shadow_memory |
| Shadow memory instrumentation API.
|
unsigned | _total_vccs |
unsigned | _remaining_vccs |