Revision 8060f89a
Added by Lélio Brun over 3 years ago
| include/arrow_spec.h | ||
|---|---|---|
| 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_ |
|
Also available in: Unified diff
forgotten file