symex_main.cpp File Reference

Symbolic Execution. More...

#include <util/exception_utils.h>
#include <util/expr_iterator.h>
#include <util/expr_util.h>
#include <util/format.h>
#include <util/format_expr.h>
#include <util/invariant.h>
#include <util/magic.h>
#include <util/mathematical_expr.h>
#include <util/replace_symbol.h>
#include <util/std_expr.h>
#include <pointer-analysis/value_set_dereference.h>
#include "goto_symex.h"
#include "path_storage.h"
#include <memory>

Include dependency graph for symex_main.cpp:

Go to the source code of this file.

Functions
static void	pop_exited_loops (const goto_programt::const_targett &to, std::vector< framet::active_loop_infot > &active_loops)
	If 'to' is not an instruction in our currently top-most active loop, pop and re-check until we find an loop we're still active in, or empty the stack. More...
void	symex_transition (goto_symext::statet &state, goto_programt::const_targett to, bool is_backwards_goto)
void	symex_transition (goto_symext::statet &state)
	Transition to the next instruction, which increments the internal program counter and initializes the loop counter when it detects a loop (or recursion) being entered. More...
static void	switch_to_thread (goto_symex_statet &state, const unsigned int thread_nb)
static std::optional< symbol_exprt >	find_unique_pointer_typed_symbol (const exprt &expr)
	Check if an expression only contains one unique symbol (possibly repeated multiple times) More...

Detailed Description

Symbolic Execution.

Definition in file symex_main.cpp.

Function Documentation

find_unique_pointer_typed_symbol()

static std::optional<symbol_exprt> find_unique_pointer_typed_symbol ( const exprt &  expr )

static

Check if an expression only contains one unique symbol (possibly repeated multiple times)

Parameters

expr	The expression to examine

Returns

If only one unique symbol occurs in expr then return it; otherwise return an empty std::optional

Definition at line 757 of file symex_main.cpp.

pop_exited_loops()

static void pop_exited_loops ( const goto_programt::const_targett &  to, std::vector< framet::active_loop_infot > &  active_loops  )

static

If 'to' is not an instruction in our currently top-most active loop, pop and re-check until we find an loop we're still active in, or empty the stack.

Definition at line 60 of file symex_main.cpp.

switch_to_thread()

static void switch_to_thread ( goto_symex_statet &  state, const unsigned int  thread_nb  )

static

Definition at line 279 of file symex_main.cpp.

symex_transition() [1/2]

void symex_transition

(

goto_symext::statet &

state

)

Transition to the next instruction, which increments the internal program counter and initializes the loop counter when it detects a loop (or recursion) being entered.

'Next instruction' in this situation refers to the next one in program order, so it ignores things like unconditional GOTOs, and only goes until the end of the current function.

Parameters

state

Symbolic execution state to be transformed

Definition at line 144 of file symex_main.cpp.

symex_transition() [2/2]

void symex_transition	(	goto_symext::statet &	state,
		goto_programt::const_targett	to,
		bool	is_backwards_goto
	)

Definition at line 73 of file symex_main.cpp.