interval_abstract_value.cpp File Reference

#include <ostream>
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/expr_util.h>
#include <util/invariant.h>
#include <util/simplify_expr.h>
#include "abstract_environment.h"
#include "abstract_object_statistics.h"
#include "interval_abstract_value.h"
#include "widened_range.h"

Include dependency graph for interval_abstract_value.cpp:

Go to the source code of this file.

Classes
class	interval_index_ranget

Functions
static index_range_implementation_ptrt	make_interval_index_range (const constant_interval_exprt &interval, const namespacet &n)
static bool	bvint_value_is_max (const typet &type, const mp_integer &value)
static bool	bvint_value_is_min (const typet &type, const mp_integer &value)
static constant_interval_exprt	interval_from_x_le_value (const exprt &value)
static constant_interval_exprt	interval_from_x_ge_value (const exprt &value)
static mp_integer	force_value_from_expr (const exprt &value)
static constant_interval_exprt	interval_from_x_lt_value (const exprt &value)
static constant_interval_exprt	interval_from_x_gt_value (const exprt &value)
static bool	represents_interval (const exprt &expr)
static constant_interval_exprt	make_interval_expr (const exprt &expr)
static irep_idt	invert_relation (const irep_idt &relation)
static constant_interval_exprt	interval_from_relation (const exprt &e)
	Builds an interval representing all values satisfying the input expression.
bool	new_interval_is_top (const constant_interval_exprt &e)
abstract_object_pointert	widening_merge (const constant_interval_exprt &lhs, const constant_interval_exprt &rhs)

Function Documentation

bvint_value_is_max()

static bool bvint_value_is_max ( const typet &  type, const mp_integer &  value  )

inlinestatic

Definition at line 78 of file interval_abstract_value.cpp.

bvint_value_is_min()

static bool bvint_value_is_min ( const typet &  type, const mp_integer &  value  )

inlinestatic

Definition at line 92 of file interval_abstract_value.cpp.

force_value_from_expr()

static mp_integer force_value_from_expr ( const exprt &  value )

inlinestatic

Definition at line 117 of file interval_abstract_value.cpp.

interval_from_relation()

static constant_interval_exprt interval_from_relation ( const exprt &  e )

inlinestatic

Builds an interval representing all values satisfying the input expression.

The expression is expected to be a comparison between an integer constant and a variable (symbol)

Parameters

e	the relation expression that should be satisfied

Returns

the constant interval expression representing the values

Definition at line 196 of file interval_abstract_value.cpp.

interval_from_x_ge_value()

static constant_interval_exprt interval_from_x_ge_value ( const exprt &  value )

inlinestatic

Definition at line 112 of file interval_abstract_value.cpp.

interval_from_x_gt_value()

static constant_interval_exprt interval_from_x_gt_value ( const exprt &  value )

inlinestatic

Definition at line 139 of file interval_abstract_value.cpp.

interval_from_x_le_value()

static constant_interval_exprt interval_from_x_le_value ( const exprt &  value )

inlinestatic

Definition at line 106 of file interval_abstract_value.cpp.

interval_from_x_lt_value()

static constant_interval_exprt interval_from_x_lt_value ( const exprt &  value )

inlinestatic

Definition at line 127 of file interval_abstract_value.cpp.

invert_relation()

static irep_idt invert_relation ( const irep_idt &  relation )

inlinestatic

Definition at line 175 of file interval_abstract_value.cpp.

make_interval_expr()

static constant_interval_exprt make_interval_expr ( const exprt &  expr )

inlinestatic

Definition at line 156 of file interval_abstract_value.cpp.

make_interval_index_range()

static index_range_implementation_ptrt make_interval_index_range ( const constant_interval_exprt &  interval, const namespacet &  n  )

static

Definition at line 70 of file interval_abstract_value.cpp.

new_interval_is_top()

bool new_interval_is_top

(

const constant_interval_exprt &

e

)

Definition at line 237 of file interval_abstract_value.cpp.

represents_interval()

static bool represents_interval ( const exprt &  expr )

inlinestatic

Definition at line 150 of file interval_abstract_value.cpp.

widening_merge()

abstract_object_pointert widening_merge	(	const constant_interval_exprt &	lhs,
		const constant_interval_exprt &	rhs
	)

Definition at line 359 of file interval_abstract_value.cpp.