Revision f2b1c245 src/normalization.ml
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