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. More...

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.

Classes

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ set_predicate_fn

Function Documentation

◆ are_any_top()

◆ collapse_overlapping_intervals()

◆ collapse_values_in_intervals()

◆ collect_intervals()

◆ compact_values()

◆ destructive_compact()

◆ eval_expr()

◆ is_eq()

◆ is_le()

◆ is_lt()

◆ is_set_extreme()

◆ make_value_set_index_range()

◆ make_value_set_value_range()

◆ maybe_extract_single_value()

◆ non_destructive_compact()

◆ set_contains()

◆ set_has_extremes()

◆ unwrap_and_extract_values()

◆ value_is_not_contained_in()

◆ widen_value_set()