Revision 0038002e src/inliner.ml
src/inliner.ml | ||
---|---|---|
134 | 134 |
let el, l', eqs' = inline_tuple (List.map snd branches) in |
135 | 135 |
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in |
136 | 136 |
{ expr with expr_desc = Expr_merge (id, branches') }, l', eqs' |
137 |
| Expr_uclock _ |
|
138 |
| Expr_dclock _ |
|
139 |
| Expr_phclock _ -> assert false |
|
140 | 137 |
and inline_node nd nodes = |
141 | 138 |
let new_locals, eqs = |
142 | 139 |
List.fold_left (fun (locals, eqs) eq -> |
... | ... | |
244 | 241 |
node_stateless = None; |
245 | 242 |
node_spec = Some |
246 | 243 |
{requires = []; |
247 |
ensures = [EnsuresExpr (mkeexpr loc (EExpr_ident ok_ident))]; |
|
248 |
behaviors = [] |
|
244 |
ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))]; |
|
245 |
behaviors = []; |
|
246 |
spec_loc = loc |
|
249 | 247 |
}; |
250 |
node_annot = None;
|
|
248 |
node_annot = [];
|
|
251 | 249 |
} |
252 | 250 |
in |
253 | 251 |
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc }] in |
Also available in: Unified diff