CBMC: /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/full_array_abstract_object.cpp File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Functions

full_array_abstract_object.cpp File Reference

#include <ostream>
#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/variable_sensitivity_configuration.h>
#include <util/arith_tools.h>
#include <util/mathematical_types.h>
#include <util/std_expr.h>
#include "abstract_value_object.h"
#include "full_array_abstract_object.h"
#include "location_update_visitor.h"
#include "map_visit.h"

+ Include dependency graph for full_array_abstract_object.cpp:

Go to the source code of this file.

Classes

struct eval_index_resultt

Functions

static eval_index_resultt eval_index (const exprt &expr, const abstract_environmentt &env, const namespacet &ns)

static eval_index_resultt eval_index (const mp_integer &index, const abstract_environmentt &env, const namespacet &ns)

template<typename index_fn >

abstract_object_pointert apply_to_index_range (const abstract_environmentt &environment, const exprt &expr, const namespacet &ns, index_fn &fn)

Function Documentation

◆ apply_to_index_range()

template<typename index_fn >

abstract_object_pointert apply_to_index_range ( const abstract_environmentt & environment,

const exprt & expr,

const namespacet & ns,

index_fn & fn

)

Definition at line 39 of file full_array_abstract_object.cpp.

◆ eval_index() [1/2]

static eval_index_resultt eval_index ( const exprt & expr,

const abstract_environmentt & env,

const namespacet & ns

)

static

Definition at line 456 of file full_array_abstract_object.cpp.

◆ eval_index() [2/2]

static eval_index_resultt eval_index ( const mp_integer & index,

const abstract_environmentt & env,

const namespacet & ns

)

static

Definition at line 476 of file full_array_abstract_object.cpp.