Project

General

Profile

Revision 4f26dcf5 src/lustre_types.ml

View differences:

src/lustre_types.ml
124 124
 {annots: (string list * eexpr) list;
125 125
  annot_loc: Location.t}
126 126

  
127
type node_annot = {
127
type contract_desc = {
128
(* TODO: 
129
   local variables 
130
   rename: assume/guarantee
131
           in behavior mode (id, requires/ensures)
132
   import contract
133
*)
134
  
128 135
  requires: eexpr list;
129 136
  ensures: eexpr list;
130 137
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
......
173 180
     node_stmts: statement list;
174 181
     mutable node_dec_stateless: bool;
175 182
     mutable node_stateless: bool option;
176
     node_spec: node_annot option;
183
     node_spec: contract_desc option;
177 184
     node_annot: expr_annot list;
178 185
    }
179 186

  
......
184 191
     nodei_inputs: var_decl list;
185 192
     nodei_outputs: var_decl list;
186 193
     nodei_stateless: bool;
187
     nodei_spec: node_annot option;
194
     nodei_spec: contract_desc option;
188 195
     (* nodei_annot: expr_annot list; *)
189 196
     nodei_prototype: string option;
190 197
     nodei_in_lib: string list;
......
204 211
| Open of bool * string (* the boolean set to true denotes a local
205 212
			   lusi vs a lusi installed at system level *)
206 213
| TypeDef of typedef_desc
207

  
214
| Contract of contract_desc
215
    
208 216
type top_decl =
209 217
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
210 218
     top_decl_owner: Location.filename; (* the module where it is defined *)

Also available in: Unified diff