Project

General

Profile

« Previous | Next » 

Revision aaa8e454

Added by LĂ©lio Brun 7 months ago

it works

View differences:

include/arrow_spec.h
44 44
                             : (mem_out._reg._first == mem_in._reg._first));
45 45
*/
46 46

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

  
52 52
/*@
53 53
  requires \separated(mem, self);
54
  requires _arrow_ghost(*mem, self);
55
  ensures  _arrow_ghost(*mem, self);
54
  requires _arrow_pack(*mem, self);
55
  ensures  _arrow_pack(*mem, self);
56 56
  ensures \result == \old(self->_reg._first);
57 57
  ensures self->_reg._first == 0;
58 58
  ensures !\old(mem->_reg._first) ==> *mem == \old(*mem);

Also available in: Unified diff