cprover
|
Symbolic Execution. More...
#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>
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... | |
Symbolic Execution.
Definition in file symex_goto.cpp.
|
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.
|
static |
Helper function for phi_function
which merges the names of an identifier for two different states.
goto_state | first state | |
[in,out] | dest_state | second state |
ns | namespace | |
diff_guard | difference between the guards of the two states | |
guard_identifier | prefix used for goto symex guards | |
[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 |
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 404 of file symex_goto.cpp.