Project

General

Profile

« Previous | Next » 

Revision 0406ab94

Added by LĂ©lio Brun 7 months ago

implement optimization on spec: IT WORKS

View differences:

include/arrow_spec.h
37 37
 */
38 38

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

Also available in: Unified diff