Project

General

Profile

« Previous | Next » 

Revision 6d1693b9

Added by LĂ©lio Brun 7 months ago

work on spec generation almost done

View differences:

include/arrow_spec.h
1 1
#ifndef ARROW_SPEC_H_
2 2
#define ARROW_SPEC_H_
3 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

  
4 29
/* ACSL arrow spec */
5 30
//@ 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;
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));
13 45
*/
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));
46

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

  
23 52
/*@
24
   predicate _arrow_ghost(struct _arrow_mem_ghost mem,
25
                          struct _arrow_mem *self) =
26
     mem._reg._first == self->_reg._first;
53
  requires \separated(mem, self);
54
  requires _arrow_ghost(*mem, self);
55
  ensures  _arrow_ghost(*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;
27 60
*/
61
_Bool _arrow_step(struct _arrow_mem *self)
62
       /*@ ghost (struct _arrow_mem_ghost \ghost *mem) */;
28 63

  
29 64
#endif // ARROW_SPEC_H_

Also available in: Unified diff