cprover
value_set_abstract_object.cpp File Reference

Value Set Abstract Object. More...

+ Include dependency graph for value_set_abstract_object.cpp:

Go to the source code of this file.

Classes

class  value_set_index_ranget
 
class  value_set_value_ranget
 

Functions

static index_range_implementation_ptrt make_value_set_index_range (const std::set< exprt > &vals)
 
static value_range_implementation_ptrt make_value_set_value_range (const abstract_object_sett &vals)
 
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. More...
 
static bool are_any_top (const abstract_object_sett &set)
 
static abstract_object_pointert maybe_unwrap_context (const abstract_object_pointert &maybe_wrapped)
 

Detailed Description

Value Set Abstract Object.

Definition in file value_set_abstract_object.cpp.

Function Documentation

◆ are_any_top()

static bool are_any_top ( const abstract_object_sett set)
static

Definition at line 344 of file value_set_abstract_object.cpp.

◆ make_value_set_index_range()

static index_range_implementation_ptrt make_value_set_index_range ( const std::set< exprt > &  vals)
static

Definition at line 56 of file value_set_abstract_object.cpp.

◆ make_value_set_value_range()

static value_range_implementation_ptrt make_value_set_value_range ( const abstract_object_sett vals)
static

Definition at line 98 of file value_set_abstract_object.cpp.

◆ maybe_extract_single_value()

static 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 328 of file value_set_abstract_object.cpp.

◆ maybe_unwrap_context()

static abstract_object_pointert maybe_unwrap_context ( const abstract_object_pointert maybe_wrapped)
static

Definition at line 306 of file value_set_abstract_object.cpp.

◆ unwrap_and_extract_values()

static abstract_object_sett unwrap_and_extract_values ( const abstract_object_sett values)
static

Definition at line 315 of file value_set_abstract_object.cpp.