Project

General

Profile

Revision f2b1c245 src/normalization.ml

View differences:

src/normalization.ml
358 358
      let assert_expr = assert_.assert_expr in
359 359
      let (defs, vars'), expr = 
360 360
	normalize_expr 
361
	  ~alias:false 
361
	  ~alias:true 
362 362
	  node 
363 363
	  [] (* empty offset for arrays *)
364 364
	  ([], vars) (* defvar only contains vars *)
365 365
	  assert_expr
366 366
      in
367
      (* Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars'; *)
367 368
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
368 369
    ) (vars, [], []) node.node_asserts in
369 370
  let new_locals = List.filter is_local vars in
371
  (* Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals; *)
372

  
370 373
  (* Compute traceability info: 
371 374
     - gather newly bound variables
372 375
     - compute the associated expression without aliases     
......
393 396
    node_asserts = asserts;
394 397
    node_annot = norm_traceability::node.node_annot;
395 398
  }
396
  in ((*Printers.pp_node Format.err_formatter node;*) node)
399
  in ((*Printers.pp_node Format.err_formatter node;*) 
400
    node
401
)
402

  
397 403

  
398 404
let normalize_decl decl =
399 405
  match decl.top_decl_desc with
400 406
  | Node nd ->
401
    {decl with top_decl_desc = Node (normalize_node nd)}
407
    let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in
408
    Hashtbl.replace Corelang.node_table nd.node_id decl';
409
    decl'
402 410
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
403 411
  
404 412
let normalize_prog decls = 

Also available in: Unified diff