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