Project

General

Profile

Revision 0038002e src/inliner.ml

View differences:

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