Revision f9f06e7d src/lustre_types.ml
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