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.