Project

General

Profile

Revision f9f06e7d src/lustre_types.ml

View differences:

src/lustre_types.ml
131 131
type contract_import =
132 132
  { import_nodeid: ident; inputs: expr list; outputs: expr list; import_loc: Location.t }
133 133
    
134
type contract_desc = 
135
  {
136
(* TODO: 
137
   local variables 
138
   rename: assume/guarantee
139
           in behavior mode (id, requires/ensures)
140
   import contract
141
*)
142
       consts: var_decl list;
143
       locals: var_decl list;
144
       assume: eexpr list;
145
       guarantees: eexpr list;
146
       modes: contract_mode list;
147
       imports: contract_import list; 
148
       spec_loc: Location.t;
149
}
150 134

  
151 135

  
152 136
type offset =
......
178 162
   hand_annots: expr_annot list;
179 163
   hand_loc: Location.t}
180 164

  
165
type contract_desc = 
166
  {
167
    consts: var_decl list;
168
    locals: var_decl list;
169
    stmts: statement list;
170
    assume: eexpr list;
171
    guarantees: eexpr list;
172
    modes: contract_mode list;
173
    imports: contract_import list; 
174
    spec_loc: Location.t;
175
  }
176

  
181 177
type node_desc =
182 178
    {node_id: ident;
183 179
     mutable node_type: Types.type_expr;

Also available in: Unified diff