Loading...

Searching...

No Matches

symex_goto.cpp File Reference

Symbolic Execution. More...

#include <util/exception_utils.h>
#include <util/expr_util.h>
#include <util/invariant.h>
#include <util/pointer_offset_size.h>
#include <util/simplify_expr.h>
#include <util/std_expr.h>
#include <langapi/language_util.h>
#include "goto_symex.h"
#include "path_storage.h"
#include "simplify_expr_with_value_set.h"
#include <algorithm>
#include <map>

+ Include dependency graph for symex_goto.cpp:

[フレーム]

Go to the source code of this file.

Functions

static guardt merge_state_guards (goto_statet &goto_state, goto_symex_statet &state)

static void merge_names (const goto_statet &goto_state, goto_symext::statet &dest_state, const namespacet &ns, const guardt &diff_guard, messaget &log, const bool do_simplify, symex_target_equationt &target, const incremental_dirtyt &dirty, const ssa_exprt &ssa, const std::size_t goto_count, const std::size_t dest_count)

Helper function for phi_function which merges the names of an identifier for two different states.

Detailed Description

Symbolic Execution.

Definition in file symex_goto.cpp.

Function Documentation

◆ merge_names()

static void merge_names ( const goto_statet & goto_state,

goto_symext::statet & dest_state,

const namespacet & ns,

const guardt & diff_guard,

messaget & log,

const bool do_simplify,

symex_target_equationt & target,

const incremental_dirtyt & dirty,

const ssa_exprt & ssa,

const std::size_t goto_count,

const std::size_t dest_count

)

static

Helper function for phi_function which merges the names of an identifier for two different states.

Parameters: goto_state first state

[in,out] dest_state second state

ns namespace

diff_guard difference between the guards of the two states

[out] log logger for debug messages

do_simplify should the right-hand-side of the assignment that is added to the target be simplified

[out] target equation that will receive the resulting assignment

dirty dirty-object analysis

ssa SSA expression to merge

goto_count current level 2 count in goto_state of l1_identifier

dest_count level 2 count in dest_state of l1_identifier

Definition at line 575 of file symex_goto.cpp.

◆ merge_state_guards()

static guardt merge_state_guards ( goto_statet & goto_state,

goto_symex_statet & state

)

static

Definition at line 487 of file symex_goto.cpp.