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

 
 
template<typename index_fn >
 

Function Documentation

◆  apply_to_index_range()

template<typename index_fn >
abstract_object_pointert apply_to_index_range ( const abstract_environmenttenvironment,
const exprtexpr,
const namespacetns,
index_fnfn 
)

Definition at line 39 of file full_array_abstract_object.cpp.

◆  eval_index() [1/2]

static eval_index_resultt eval_index ( const exprtexpr,
const namespacetns 
)
static

Definition at line 456 of file full_array_abstract_object.cpp.

◆  eval_index() [2/2]

static eval_index_resultt eval_index ( const mp_integerindex,
const namespacetns 
)
static

Definition at line 476 of file full_array_abstract_object.cpp.

AltStyle によって変換されたページ (->オリジナル) /