|
CBMC
|
#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) |
| 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.
|
static |
Definition at line 462 of file full_array_abstract_object.cpp.
|
static |
Definition at line 482 of file full_array_abstract_object.cpp.