symex_function.cpp File Reference

#include <algorithm>
#include <cassert>
#include <string_view>
#include <unordered_set>
#include <goto-symex/scheduler/execution_state.h>
#include <goto-symex/engine/goto_symex.h>
#include <langapi/language_util.h>
#include <util/arith/arith_tools.h>
#include <util/expr/base_type.h>
#include <util/lang/c_types.h>
#include <util/symtab/cprover_prefix.h>
#include <util/expr/expr_util.h>
#include <util/base/i2string.h>
#include <util/base/prefix.h>
#include <util/symtab/pretty.h>
#include <util/lang/python_types.h>
#include <util/irep/std_expr.h>

Include dependency graph for symex_function.cpp:

Functions
static void	give_locals_fresh_instances (const goto_functiont &goto_function, goto_symex_statet &state, goto_symex_statet::framet &frame)
static bool	function_is_type_compatible (const code_type2t &declared_type, const code_type2t &candidate, const namespacet &ns)
static bool	has_call_target (const expr2tc &expr)
static std::list< std::pair< guard2tc, expr2tc > >	get_function_list (const expr2tc &expr)

Function Documentation

function_is_type_compatible()

bool function_is_type_compatible ( const code_type2t & declared_type, const code_type2t & candidate, const namespacet & ns )

static

get_function_list()

std::list< std::pair< guard2tc, expr2tc > > get_function_list ( const expr2tc & expr )

static

give_locals_fresh_instances()

void give_locals_fresh_instances ( const goto_functiont & goto_function, goto_symex_statet & state, goto_symex_statet::framet & frame )

static

has_call_target()

bool has_call_target ( const expr2tc & expr )

static