Project

General

Profile

« Previous | Next » 

Revision 27502d69

Added by LĂ©lio Brun 7 months ago

add memory instances to footprint lemmas

View differences:

src/spec_types.ml
39 39
      (* outputs *)
40 40
      * bool (* reset *)
41 41
      * Utils.ISet.t (* memory footprint *)
42
      * ident Utils.IMap.t
43
      (* memory instances footprint *)
42 44
      -> 'a predicate_t
43 45
  | Reset of ident * ident * 'a
44 46
  | MemoryPack of ident * ident option * int option
......
80 82
  tlocals : var_decl list;
81 83
  toutputs : var_decl list;
82 84
  tformula : 'a formula_t;
83
  tfootprint : Utils.ISet.t;
85
  tmem_footprint : Utils.ISet.t;
86
  tinst_footprint : ident Utils.IMap.t;
84 87
}

Also available in: Unified diff