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 
10 
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:
25 };
26 
28 {
29 public:
31  {
32  }
33 };
34 
36  : value(val), available(true)
37 {
38 }
39 
41 {
42  return value;
43 }
44 
46 {
47  bool a = available;
48  available = false;
49  return a;
50 }
51 
53 {
54  return std::make_shared<empty_index_ranget>();
55 }
56 
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.