cprover
abstract_value_object.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: analyses variable-sensitivity
4
5
Author: Jez Higgins, jez@jezuk.co.uk
6
7
\*******************************************************************/
8
9
#include <
analyses/variable-sensitivity/abstract_value_object.h
>
10
11
class
empty_index_ranget
:
public
index_ranget
12
{
13
public
:
14
const
exprt
&
current
()
const override
15
{
16
return
nil
;
17
}
18
bool
advance_to_next
()
override
19
{
20
return
false
;
21
}
22
23
private
:
24
exprt
nil
=
nil_exprt
();
25
};
26
27
class
indeterminate_index_ranget
:
public
single_value_index_ranget
28
{
29
public
:
30
indeterminate_index_ranget
() :
single_value_index_ranget
(
nil_exprt
())
31
{
32
}
33
};
34
35
single_value_index_ranget::single_value_index_ranget
(
const
exprt
&val)
36
: value(val), available(true)
37
{
38
}
39
40
const
exprt
&
single_value_index_ranget::current
()
const
41
{
42
return
value
;
43
}
44
45
bool
single_value_index_ranget::advance_to_next
()
46
{
47
bool
a =
available
;
48
available
=
false
;
49
return
a;
50
}
51
52
index_range_ptrt
make_empty_index_range
()
53
{
54
return
std::make_shared<empty_index_ranget>();
55
}
56
57
index_range_ptrt
make_indeterminate_index_range
()
58
{
59
return
std::make_shared<indeterminate_index_ranget>();
60
}
index_ranget
Definition:
abstract_value_object.h:22
single_value_index_ranget
Definition:
abstract_value_object.h:30
indeterminate_index_ranget::indeterminate_index_ranget
indeterminate_index_ranget()
Definition:
abstract_value_object.cpp:30
single_value_index_ranget::current
const exprt & current() const override
Definition:
abstract_value_object.cpp:40
exprt
Base class for all expressions.
Definition:
expr.h:54
single_value_index_ranget::value
const exprt value
Definition:
abstract_value_object.h:39
index_range_ptrt
std::shared_ptr< index_ranget > index_range_ptrt
Definition:
abstract_value_object.h:43
empty_index_ranget
Definition:
abstract_value_object.cpp:12
indeterminate_index_ranget
Definition:
abstract_value_object.cpp:28
single_value_index_ranget::single_value_index_ranget
single_value_index_ranget(const exprt &val)
Definition:
abstract_value_object.cpp:35
make_indeterminate_index_range
index_range_ptrt make_indeterminate_index_range()
Definition:
abstract_value_object.cpp:57
nil_exprt
The NIL expression.
Definition:
std_expr.h:2735
make_empty_index_range
index_range_ptrt make_empty_index_range()
Definition:
abstract_value_object.cpp:52
empty_index_ranget::current
const exprt & current() const override
Definition:
abstract_value_object.cpp:14
single_value_index_ranget::available
bool available
Definition:
abstract_value_object.h:40
single_value_index_ranget::advance_to_next
bool advance_to_next() override
Definition:
abstract_value_object.cpp:45
empty_index_ranget::nil
exprt nil
Definition:
abstract_value_object.cpp:24
empty_index_ranget::advance_to_next
bool advance_to_next() override
Definition:
abstract_value_object.cpp:18
abstract_value_object.h
Common behaviour for abstract objects modelling values - constants, intervals, etc.
analyses
variable-sensitivity
abstract_value_object.cpp
Generated by
1.8.20