CBMC
Loading...
Searching...
No Matches
sentinel_dll.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Sentinel Doubly Linked Lists
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_CPROVER_SENTINEL_DLL_H
10#define CPROVER_CPROVER_SENTINEL_DLL_H
11
12#include <util/std_expr.h>
13
15{
16public:
27
31 {state, head, tail, node},
32 bool_typet())
33 {
34 PRECONDITION(this->state().type().id() == ID_state);
35 PRECONDITION(this->head().type().id() == ID_pointer);
36 PRECONDITION(this->tail().type().id() == ID_pointer);
37 }
38
39 const exprt &state() const
40 {
41 return op0();
42 }
43
45 {
46 return op0();
47 }
48
49 const exprt &head() const
50 {
51 return op1();
52 }
53
55 {
56 return op1();
57 }
58
59 const exprt &tail() const
60 {
61 return op2();
62 }
63
65 {
66 return op2();
67 }
68
69 // helper
71 {
72 auto result = *this; // copy
73 result.state() = std::move(state);
74 return result;
75 }
76};
77
84inline const state_is_sentinel_dll_exprt &
86{
89 static_cast<const state_is_sentinel_dll_exprt &>(expr);
91 return ret;
92}
93
103
104std::optional<exprt>
105sentinel_dll_next(const exprt &state, const exprt &node, const namespacet &);
106
107std::optional<exprt>
108sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &);
109
110#endif // CPROVER_CPROVER_SENTINEL_DLL_H
void validate_expr(const shuffle_vector_exprt &value)
Definition c_expr.h:82
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
The Boolean type.
Definition std_types.h:36
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
const irep_idt & id() const
Definition irep.h:388
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:912
exprt & op1()
Definition std_expr.h:938
exprt & op0()
Definition std_expr.h:932
exprt & op2()
Definition std_expr.h:944
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
state_is_sentinel_dll_exprt(exprt state, exprt head, exprt tail, exprt node)
const exprt & head() const
const exprt & state() const
state_is_sentinel_dll_exprt with_state(exprt state) const
state_is_sentinel_dll_exprt(exprt state, exprt head, exprt tail)
const exprt & tail() const
std::optional< exprt > sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &)
const state_is_sentinel_dll_exprt & to_state_is_sentinel_dll_expr(const exprt &expr)
Cast an exprt to a state_is_sentinel_dll_exprt.
std::optional< exprt > sentinel_dll_next(const exprt &state, const exprt &node, const namespacet &)
#define PRECONDITION(CONDITION)
Definition invariant.h:463
API to expression classes.