|
1
|
#ifndef ARROW_SPEC_H_
|
|
2
|
#define ARROW_SPEC_H_
|
|
3
|
|
|
4
|
/* ACSL arrow spec */
|
|
5
|
//@ ghost struct _arrow_mem_ghost {struct _arrow_reg _reg;};
|
|
6
|
/*@
|
|
7
|
predicate _arrow_valid(struct _arrow_mem *self) =
|
|
8
|
\valid(self);
|
|
9
|
*/
|
|
10
|
/*@
|
|
11
|
predicate _arrow_initialization(struct _arrow_mem_ghost mem_in) =
|
|
12
|
mem_in._reg._first == 1;
|
|
13
|
*/
|
|
14
|
/*@
|
|
15
|
predicate _arrow_transition(struct _arrow_mem_ghost mem_in,
|
|
16
|
integer x, integer y,
|
|
17
|
struct _arrow_mem_ghost mem_out, _Bool out) =
|
|
18
|
(mem_in._reg._first ? (mem_out._reg._first == 0
|
|
19
|
&& out == x)
|
|
20
|
: (mem_out._reg._first == mem_in._reg._first
|
|
21
|
&& out == y));
|
|
22
|
*/
|
|
23
|
/*@
|
|
24
|
predicate _arrow_ghost(struct _arrow_mem_ghost mem,
|
|
25
|
struct _arrow_mem *self) =
|
|
26
|
mem._reg._first == self->_reg._first;
|
|
27
|
*/
|
|
28
|
|
|
29
|
#endif // ARROW_SPEC_H_
|