CBMC
Classes | Functions
abstract_value_object.cpp File Reference
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/ieee_float.h>
#include <util/simplify_expr.h>
#include <goto-programs/adjust_float_expressions.h>
#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/abstract_value_object.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 "context_abstract_object.h"
#include <algorithm>
+ Include dependency graph for abstract_value_object.cpp:

Go to the source code of this file.

Classes

class  empty_index_ranget
 
class  indeterminate_index_ranget
 
class  single_value_value_ranget
 
class  constants_evaluator
 
class  interval_evaluator
 
class  value_set_evaluator
 

Functions

index_range_implementation_ptrt make_empty_index_range ()
 
index_range_implementation_ptrt make_indeterminate_index_range ()
 
value_range_implementation_ptrt make_single_value_range (const abstract_object_pointert &value)
 
static abstract_object_pointert constants_expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
 
static abstract_object_pointert intervals_expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
 
static abstract_object_pointert value_set_expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
 
template<class representation_type >
bool any_of_type (const std::vector< abstract_object_pointert > &operands)
 
bool any_value_sets (const std::vector< abstract_object_pointert > &operands)
 
bool any_intervals (const std::vector< abstract_object_pointert > &operands)
 
static abstract_object_pointert transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
 
template<class representation_type >
abstract_object_pointert make_top (const typet &type)
 

Function Documentation

◆ any_intervals()

bool any_intervals ( const std::vector< abstract_object_pointert > &  operands)

Definition at line 154 of file abstract_value_object.cpp.

◆ any_of_type()

template<class representation_type >
bool any_of_type ( const std::vector< abstract_object_pointert > &  operands)

Definition at line 137 of file abstract_value_object.cpp.

◆ any_value_sets()

bool any_value_sets ( const std::vector< abstract_object_pointert > &  operands)

Definition at line 149 of file abstract_value_object.cpp.

◆ constants_expression_transform()

abstract_object_pointert constants_expression_transform ( const exprt &  expr,
const std::vector< abstract_object_pointert > &  operands,
const abstract_environmentt &  environment,
const namespacet &  ns 
)
static

Definition at line 375 of file abstract_value_object.cpp.

◆ intervals_expression_transform()

abstract_object_pointert intervals_expression_transform ( const exprt &  expr,
const std::vector< abstract_object_pointert > &  operands,
const abstract_environmentt &  environment,
const namespacet &  ns 
)
static

Definition at line 538 of file abstract_value_object.cpp.

◆ make_empty_index_range()

index_range_implementation_ptrt make_empty_index_range ( )

Definition at line 76 of file abstract_value_object.cpp.

◆ make_indeterminate_index_range()

index_range_implementation_ptrt make_indeterminate_index_range ( )

Definition at line 81 of file abstract_value_object.cpp.

◆ make_single_value_range()

value_range_implementation_ptrt make_single_value_range ( const abstract_object_pointert &  value)

Definition at line 115 of file abstract_value_object.cpp.

◆ make_top()

template<class representation_type >
abstract_object_pointert make_top ( const typet &  type)

Definition at line 217 of file abstract_value_object.cpp.

◆ transform()

static abstract_object_pointert transform ( const exprt &  expr,
const std::vector< abstract_object_pointert > &  operands,
const abstract_environmentt &  environment,
const namespacet &  ns 
)
static

Definition at line 159 of file abstract_value_object.cpp.

◆ value_set_expression_transform()

static abstract_object_pointert value_set_expression_transform ( const exprt &  expr,
const std::vector< abstract_object_pointert > &  operands,
const abstract_environmentt &  environment,
const namespacet &  ns 
)
static

Definition at line 686 of file abstract_value_object.cpp.