CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Classes | Typedefs | Functions
value_set_abstract_object.cpp File Reference

Value Set Abstract Object. More...

#include <util/arith_tools.h>
#include <util/simplify_expr.h>
#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/constant_abstract_value.h>
#include <analyses/variable-sensitivity/interval_abstract_value.h>
#include <analyses/variable-sensitivity/value_set_abstract_object.h>
#include <analyses/variable-sensitivity/widened_range.h>
#include "context_abstract_object.h"
#include <algorithm>
+ 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
 

Typedefs

using set_predicate_fn = std::function< bool(const abstract_value_objectt &)>
 

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.
 
static bool are_any_top (const abstract_object_sett &set)
 
static bool is_set_extreme (const typet &type, const abstract_object_sett &set)
 
static abstract_object_sett compact_values (const abstract_object_sett &values)
 
static abstract_object_sett non_destructive_compact (const abstract_object_sett &values)
 
static abstract_object_sett widen_value_set (const abstract_object_sett &values, const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)
 
static bool set_contains (const abstract_object_sett &set, set_predicate_fn pred)
 
static bool set_has_extremes (const abstract_object_sett &set, set_predicate_fn lower_fn, set_predicate_fn upper_fn)
 
static abstract_object_sett destructive_compact (abstract_object_sett values, int slice=3)
 
static bool value_is_not_contained_in (const abstract_object_pointert &object, const std::vector< constant_interval_exprt > &intervals)
 
static exprt eval_expr (const exprt &e)
 
static bool is_eq (const exprt &lhs, const exprt &rhs)
 
static bool is_le (const exprt &lhs, const exprt &rhs)
 
static bool is_lt (const exprt &lhs, const exprt &rhs)
 
static abstract_object_sett collapse_values_in_intervals (const abstract_object_sett &values, const std::vector< constant_interval_exprt > &intervals)
 
static void collapse_overlapping_intervals (std::vector< constant_interval_exprt > &intervals)
 
static std::vector< constant_interval_exprt > collect_intervals (const abstract_object_sett &values)
 

Detailed Description

Value Set Abstract Object.

Definition in file value_set_abstract_object.cpp.

Typedef Documentation

◆ set_predicate_fn

using set_predicate_fn = std::function<bool(const abstract_value_objectt &)>

Definition at line 410 of 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 402 of file value_set_abstract_object.cpp.

◆ collapse_overlapping_intervals()

void collapse_overlapping_intervals ( std::vector< constant_interval_exprt > &  intervals)
static

Definition at line 520 of file value_set_abstract_object.cpp.

◆ collapse_values_in_intervals()

static abstract_object_sett collapse_values_in_intervals ( const abstract_object_sett &  values,
const std::vector< constant_interval_exprt > &  intervals 
)
static

Definition at line 562 of file value_set_abstract_object.cpp.

◆ collect_intervals()

static std::vector< constant_interval_exprt > collect_intervals ( const abstract_object_sett &  values)
static

Definition at line 503 of file value_set_abstract_object.cpp.

◆ compact_values()

static abstract_object_sett compact_values ( const abstract_object_sett &  values)
static

Definition at line 478 of file value_set_abstract_object.cpp.

◆ destructive_compact()

static abstract_object_sett destructive_compact ( abstract_object_sett  values,
int  slice = 3 
)
static

Definition at line 587 of file value_set_abstract_object.cpp.

◆ eval_expr()

static exprt eval_expr ( const exprt &  e)
static

Definition at line 631 of file value_set_abstract_object.cpp.

◆ is_eq()

static bool is_eq ( const exprt &  lhs,
const exprt &  rhs 
)
static

Definition at line 639 of file value_set_abstract_object.cpp.

◆ is_le()

static bool is_le ( const exprt &  lhs,
const exprt &  rhs 
)
static

Definition at line 644 of file value_set_abstract_object.cpp.

◆ is_lt()

static bool is_lt ( const exprt &  lhs,
const exprt &  rhs 
)
static

Definition at line 649 of file value_set_abstract_object.cpp.

◆ is_set_extreme()

static bool is_set_extreme ( const typet &  type,
const abstract_object_sett &  set 
)
static

Definition at line 436 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 62 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 104 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 386 of file value_set_abstract_object.cpp.

◆ non_destructive_compact()

static abstract_object_sett non_destructive_compact ( const abstract_object_sett &  values)
static

Definition at line 553 of file value_set_abstract_object.cpp.

◆ set_contains()

static bool set_contains ( const abstract_object_sett &  set,
set_predicate_fn  pred 
)
static

Definition at line 411 of file value_set_abstract_object.cpp.

◆ set_has_extremes()

static bool set_has_extremes ( const abstract_object_sett &  set,
set_predicate_fn  lower_fn,
set_predicate_fn  upper_fn 
)
static

Definition at line 423 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 376 of file value_set_abstract_object.cpp.

◆ value_is_not_contained_in()

static bool value_is_not_contained_in ( const abstract_object_pointert &  object,
const std::vector< constant_interval_exprt > &  intervals 
)
static

Definition at line 616 of file value_set_abstract_object.cpp.

◆ widen_value_set()

static abstract_object_sett widen_value_set ( const abstract_object_sett &  values,
const constant_interval_exprt &  lhs,
const constant_interval_exprt &  rhs 
)
static

Definition at line 654 of file value_set_abstract_object.cpp.