Project

General

Profile

Revision 50dadc21

View differences:

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