|
CBMC
|
Value Set of Pointer Abstract Object. More...
#include <util/pointer_expr.h>#include <util/simplify_expr.h>#include <analyses/variable-sensitivity/constant_pointer_abstract_object.h>#include <analyses/variable-sensitivity/value_set_pointer_abstract_object.h>#include "abstract_environment.h"#include "context_abstract_object.h"#include <algorithm>#include <numeric>
Include dependency graph for value_set_pointer_abstract_object.cpp:Go to the source code of this file.
Functions | |
| static abstract_object_sett | unwrap_and_extract_values (const abstract_object_sett &values) |
| static abstract_object_pointert | maybe_extract_single_value (const abstract_object_pointert &maybe_singleton) |
| Helper for converting singleton value sets into its only value. | |
Value Set of Pointer Abstract Object.
Definition in file value_set_pointer_abstract_object.cpp.
|
static |
Helper for converting singleton value sets into its only value.
maybe_singleton: either a set of abstract values or a single value
Definition at line 291 of file value_set_pointer_abstract_object.cpp.
|
static |
Definition at line 279 of file value_set_pointer_abstract_object.cpp.