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 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 573 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 485 of file symex_goto.cpp.