symex_goto.cpp File Reference

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>

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