Revision 50dadc21
src/normalization.ml  

395  395 
let normalize_node node = 
396  396 
cpt_fresh := 0; 
397  397 
let inputs_outputs = node.node_inputs@node.node_outputs in 
398 
let is_local v = 

399 
List.for_all ((!=) v) inputs_outputs in 

400  398 
let orig_vars = inputs_outputs@node.node_locals in 
399 
let not_is_orig_var v = 

400 
List.for_all ((!=) v) orig_vars in 

401  401 
let defs, vars = 
402  402 
let eqs, auts = get_node_eqs node in 
403  403 
if auts != [] then assert false; (* Automata should be expanded by now. *) 
...  ...  
405  405 
(* Normalize the asserts *) 
406  406 
let vars, assert_defs, asserts = 
407  407 
List.fold_left ( 
408 
fun (vars, def_accu, assert_accu) assert_ > 

409 
let assert_expr = assert_.assert_expr in


410 
let (defs, vars'), expr =


411 
normalize_expr 

412 
~alias:true (* forcing introduction of new equations for fcn calls *) 

413 
node 

414 
[] (* empty offset for arrays *) 

415 
([], vars) (* defvar only contains vars *) 

416 
assert_expr 

417 
in


408 
fun (vars, def_accu, assert_accu) assert_ >


409 
let assert_expr = assert_.assert_expr in


410 
let (defs, vars'), expr =


411 
normalize_expr


412 
~alias:true (* forcing introduction of new equations for fcn calls *)


413 
node


414 
[] (* empty offset for arrays *)


415 
([], vars) (* defvar only contains vars *)


416 
assert_expr


417 
in


418  418 
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*) 
419 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu


419 
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu


420  420 
) (vars, [], []) node.node_asserts in 
421 
let new_locals = List.filter is_local vars in 

421 
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout 

422 
vars and initial locals ones *) 

423 
let new_locals = node.node_locals @ new_locals in (* we add again, at the 

424 
beginning of the list the 

425 
local declared ones *) 

422  426 
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*) 
423  427  
424  428 
let new_annots = 
...  ...  
454  458 
in 
455  459  
456  460 
let node = 
457 
{ node with 

458 
node_locals = new_locals; 

459 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs); 

460 
node_asserts = asserts; 

461 
node_annot = new_annots; 

462 
} 

461 
{ node with


462 
node_locals = new_locals;


463 
node_stmts = List.map (fun eq > Eq eq) (defs @ assert_defs);


464 
node_asserts = asserts;


465 
node_annot = new_annots;


466 
}


463  467 
in ((*Printers.pp_node Format.err_formatter node;*) 
464  468 
node 
465 
) 

469 
)


466  470  
467  471  
468  472 
let normalize_decl decl = 
Also available in: Unified diff