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()

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()

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.