Project

General

Profile

Download (1.71 KB) Statistics
| Branch: | Tag: | Revision:
1
#ifndef ARROW_SPEC_H_
2
#define ARROW_SPEC_H_
3

    
4
struct _arrow_mem {
5
  struct _arrow_reg {_Bool _first; } _reg;
6
};
7

    
8
extern struct _arrow_mem *_arrow_alloc ();
9

    
10
extern void _arrow_dealloc (struct _arrow_mem *);
11

    
12
#define _arrow_DECLARE(attr, inst)\
13
  attr struct _arrow_mem inst;
14

    
15
#define _arrow_LINK(inst) do {\
16
  ;\
17
} while (0)
18

    
19
#define _arrow_ALLOC(attr, inst)\
20
  _arrow_DECLARE(attr, inst);\
21
  _arrow_LINK(inst)
22

    
23
#define _arrow_init(self) {}
24

    
25
#define _arrow_clear(self) {}
26

    
27
#define _arrow_reset(self) {(self)->_reg._first = 1;}
28

    
29
/* ACSL arrow spec */
30
//@ ghost struct _arrow_mem_ghost {struct _arrow_reg _reg;};
31

    
32
#define _arrow_reset_ghost(mem) (mem)._reg._first = 1
33
#define _arrow_step_ghost(mem) (mem)._reg._first = 0
34

    
35
/*@ predicate _arrow_initialization(struct _arrow_mem_ghost mem_in) =
36
      mem_in._reg._first == 1;
37
 */
38

    
39
/*@ predicate _arrow_transition(struct _arrow_mem_ghost mem_in,
40
                                struct _arrow_mem_ghost mem_out,
41
                                _Bool out) =
42
      out == mem_in._reg._first
43
      && (mem_in._reg._first ? (mem_out._reg._first == 0)
44
                             : (mem_out._reg._first == mem_in._reg._first));
45
*/
46

    
47
/*@ predicate _arrow_pack(struct _arrow_mem_ghost mem,
48
                          struct _arrow_mem *self) =
49
      mem._reg._first == self->_reg._first;
50
*/
51

    
52
/*@
53
  requires \separated(mem, self);
54
  requires _arrow_pack(*mem, self);
55
  ensures  _arrow_pack(*mem, self);
56
  ensures \result == \old(self->_reg._first);
57
  ensures self->_reg._first == 0;
58
  ensures !\old(mem->_reg._first) ==> *mem == \old(*mem);
59
  assigns mem->_reg._first, self->_reg._first;
60
*/
61
_Bool _arrow_step(struct _arrow_mem *self)
62
       /*@ ghost (struct _arrow_mem_ghost \ghost *mem) */;
63

    
64
#endif // ARROW_SPEC_H_
(7-7/20)