CBMC
Classes | Functions
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. More...
 
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
ethe 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.