symex_main.cpp File Reference

#include <cassert>
#include <optional>
#include <goto-symex/scheduler/execution_state.h>
#include <goto-symex/engine/goto_symex.h>
#include <goto-symex/state/goto_symex_state.h>
#include <goto-symex/scheduler/reachability_tree.h>
#include <goto-symex/equation/symex_target_equation.h>
#include <langapi/language_util.h>
#include <pointer-analysis/value_set_analysis.h>
#include <util/arith/arith_tools.h>
#include <util/lang/c_types.h>
#include <util/config/config.h>
#include <util/expr/expr_util.h>
#include <irep2/irep2.h>
#include <util/irep/migrate.h>
#include <util/base/prefix.h>
#include <util/symtab/pretty.h>
#include <util/irep/std_expr.h>
#include <util/base/time_stopping.h>
#include <util/expr/type_byte_size.h>
#include <util/message/message.h>
#include <map>
#include <vector>

Include dependency graph for symex_main.cpp:

Functions
static void	havoc_modelled_writes (std::optional< interval_domaint > &domain, bool reachable, const code_function_call2t &call)
static void	require_new_object_pointer_lvalue (const code_function_call2t &func_call)

Function Documentation

havoc_modelled_writes()

void havoc_modelled_writes ( std::optional< interval_domaint > & domain, bool reachable, const code_function_call2t & call )

static

require_new_object_pointer_lvalue()

void require_new_object_pointer_lvalue ( const code_function_call2t & func_call )

static