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

CBMC

Loading...

Searching...

No Matches

value_set_pointer_abstract_object.cpp File Reference

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.

Detailed Description

Value Set of Pointer Abstract Object.

Definition in file value_set_pointer_abstract_object.cpp.

Function Documentation

◆ maybe_extract_single_value()

abstract_object_pointert maybe_extract_single_value ( const abstract_object_pointert & maybe_singleton )

static

Helper for converting singleton value sets into its only value.

maybe_singleton: either a set of abstract values or a single value

Returns: an abstract value without context

Definition at line 291 of file value_set_pointer_abstract_object.cpp.

◆ unwrap_and_extract_values()

abstract_object_sett unwrap_and_extract_values ( const abstract_object_sett & values )

static

Definition at line 279 of file value_set_pointer_abstract_object.cpp.