Loading...

Searching...

No Matches

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.

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.

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)

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 758 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.