Project

General

Profile

« Previous | Next » 

Revision 8060f89a

Added by LĂ©lio Brun about 2 years ago

forgotten file

View differences:

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