CBMC: /home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/abstract_value_object.cpp File Reference

CBMC

Loading...

Searching...

No Matches

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.