cprover
interval_abstract_value.cpp File Reference
#include <limits.h>
#include <ostream>
#include <util/invariant.h>
#include <util/std_expr.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_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 74 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 88 of file interval_abstract_value.cpp.

◆ force_value_from_expr()

static mp_integer force_value_from_expr ( const exprt value)
inlinestatic

Definition at line 113 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 188 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 108 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 133 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 102 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 122 of file interval_abstract_value.cpp.

◆ invert_relation()

static irep_idt invert_relation ( const irep_idt relation)
inlinestatic

Definition at line 167 of file interval_abstract_value.cpp.

◆ look_through_casts()

static exprt look_through_casts ( exprt  e)
inlinestatic

Definition at line 64 of file interval_abstract_value.cpp.

◆ make_interval_expr()

static constant_interval_exprt make_interval_expr ( exprt  e)
inlinestatic

Definition at line 149 of file interval_abstract_value.cpp.

◆ make_interval_index_range()

static index_range_ptrt make_interval_index_range ( const constant_interval_exprt interval,
const namespacet n 
)
static

Definition at line 57 of file interval_abstract_value.cpp.

◆ represents_interval()

static bool represents_interval ( exprt  e)
inlinestatic

Definition at line 143 of file interval_abstract_value.cpp.