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