cprover
symex_goto.cpp File Reference
#include "goto_symex.h"
#include <algorithm>
#include <util/exception_utils.h>
#include <util/expr_util.h>
#include <util/invariant.h>
#include <util/pointer_offset_size.h>
#include <util/std_expr.h>
#include <analyses/dirty.h>
#include <util/simplify_expr.h>
+ Include dependency graph for symex_goto.cpp:

Go to the source code of this file.

Functions

static void for_each2 (const std::map< irep_idt, std::pair< ssa_exprt, unsigned >> &first_map, const std::map< irep_idt, std::pair< ssa_exprt, unsigned >> &second_map, const std::function< void(const ssa_exprt &, unsigned, unsigned)> &f)
 Applies f to (k, ssa, i, j) if the first map maps k to (ssa, i) and the second to (ssa', j). More...
 
static void merge_names (const goto_symext::statet::goto_statet &goto_state, goto_symext::statet &dest_state, const namespacet &ns, const guardt &diff_guard, const irep_idt &guard_identifier, messaget &log, const bool do_simplify, symex_target_equationt &target, const ssa_exprt &ssa, const unsigned goto_count, const unsigned dest_count)
 Helper function for phi_function which merges the names of an identifier for two different states. More...
 

Detailed Description

Symbolic Execution

Definition in file symex_goto.cpp.

Function Documentation

◆ for_each2()

static void for_each2 ( const std::map< irep_idt, std::pair< ssa_exprt, unsigned >> &  first_map,
const std::map< irep_idt, std::pair< ssa_exprt, unsigned >> &  second_map,
const std::function< void(const ssa_exprt &, unsigned, unsigned)> &  f 
)
static

Applies f to (k, ssa, i, j) if the first map maps k to (ssa, i) and the second to (ssa', j).

If the first map has an entry for k but not the second one then j is 0, and when the first map has no entry for k then i = 0

Definition at line 359 of file symex_goto.cpp.

◆ merge_names()

static void merge_names ( const goto_symext::statet::goto_statet goto_state,
goto_symext::statet dest_state,
const namespacet ns,
const guardt diff_guard,
const irep_idt guard_identifier,
messaget log,
const bool  do_simplify,
symex_target_equationt target,
const ssa_exprt ssa,
const unsigned  goto_count,
const unsigned  dest_count 
)
static

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

Parameters
goto_statefirst state
[in,out]dest_statesecond state
nsnamespace
diff_guarddifference between the guards of the two states
guard_identifierprefix used for goto symex guards
[out]loglogger for debug messages
do_simplifyshould the right-hand-side of the assignment that is added to the target be simplified
[out]targetequation that will receive the resulting assignment
ssaSSA expression to merge
goto_countcurrent level 2 count in goto_state of l1_identifier
dest_countlevel 2 count in dest_state of l1_identifier

Definition at line 404 of file symex_goto.cpp.