cprover
interval_abstract_value.cpp File Reference
#include <limits.h>
#include <ostream>
#include <util/bitvector_types.h>
#include <util/invariant.h>
#include <util/make_unique.h>
#include "abstract_environment.h"
#include "context_abstract_object.h"
#include "interval_abstract_value.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 exprt look_through_casts (exprt e)
 
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 (exprt e)
 
static constant_interval_exprt make_interval_expr (exprt e)
 
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. More...
 

Function Documentation

◆ bvint_value_is_max()

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

Definition at line 86 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 100 of file interval_abstract_value.cpp.

◆ force_value_from_expr()

static mp_integer force_value_from_expr ( const exprt value)
inlinestatic

Definition at line 125 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
ethe relation expression that should be satisfied
Returns
the constant interval expression representing the values

Definition at line 200 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 120 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 145 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 114 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 134 of file interval_abstract_value.cpp.

◆ invert_relation()

static irep_idt invert_relation ( const irep_idt relation)
inlinestatic

Definition at line 179 of file interval_abstract_value.cpp.

◆ look_through_casts()

static exprt look_through_casts ( exprt  e)
inlinestatic

Definition at line 76 of file interval_abstract_value.cpp.

◆ make_interval_expr()

static constant_interval_exprt make_interval_expr ( exprt  e)
inlinestatic

Definition at line 161 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 69 of file interval_abstract_value.cpp.

◆ represents_interval()

static bool represents_interval ( exprt  e)
inlinestatic

Definition at line 155 of file interval_abstract_value.cpp.