Project

General

Profile

Revision 0d54d8a8 src/mpfr.ml

View differences:

src/mpfr.ml
211 211
  let norm_eq = { eq with eq_rhs = norm_rhs } in
212 212
  norm_eq::defs', vars'
213 213

  
214
(* let inject_eexpr ee =
215
 *   { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr }
216
 *   
217
 * let inject_spec s =
218
 *   { s with
219
 *     assume = List.map inject_eexpr s.assume;
220
 *     guarantees = List.map inject_eexpr s.guarantees;
221
 *     modes = List.map (fun m ->
222
 *                 { m with
223
 *                   require = List.map inject_eexpr m.require;
224
 *                   ensure = List.map inject_eexpr m.ensure
225
 *                 }
226
 *               ) s.modes
227
 *   } *)
228
  
214 229
(** normalize_node node returns a normalized node, 
215 230
    ie. 
216 231
    - updated locals
......
247 262
     - compute the associated expression without aliases     
248 263
  *)
249 264
  (* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)
265
  (* See comment below
266
   *  let spec = match node.node_spec with
267
   *   | None -> None
268
   *   | Some spec -> Some (inject_spec spec)
269
   * in *)
250 270
  let node =
251 271
  { node with 
252 272
    node_locals = new_locals; 
253 273
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
274
    (* Incomplete work: TODO. Do we have to inject MPFR code here?
275
       Does it make sense for annotations? For me, only if we produce
276
       C code for annotations. Otherwise the various verification
277
       backend should have their own understanding, but would not
278
       necessarily require this additional normalization. *)
279
    (* 
280
       node_spec = spec;
281
       node_annot = List.map (fun ann -> {ann with
282
           annots = List.map (fun (ids, ee) -> ids, inject_eexpr ee) ann.annots}
283
         ) node.node_annot *)
254 284
  }
255 285
  in ((*Printers.pp_node Format.err_formatter node;*) node)
256 286

  

Also available in: Unified diff