Project

General

Profile

Revision df647a81 src/machine_code.ml

View differences:

src/machine_code.ml
591 591
	   common branches are not merged while they are in C or Java
592 592
	   backends. *)
593 593
	match !Options.output with
594
	| "horn" -> s_logic
595
	| "C" | "java" | _ -> join_guards_list s_logic
594
	| "C" | "horn" -> s_logic
595
	| "java" | _ -> join_guards_list s_logic
596 596
      )
597 597
    };
598 598
    mmstep_effects = {
......
605 605
	   common branches are not merged while they are in C or Java
606 606
	   backends. *)
607 607
	match !Options.output with
608
	| "horn" -> s_side_effects
609
	| "C" | "java" | _ -> join_guards_list s_side_effects
608
	| "C" | "horn" -> s_side_effects
609
	| "java" | _ -> join_guards_list s_side_effects
610 610
      )
611 611
    }
612 612
  }    
......
664 664
  ;
665 665

  
666 666
  let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in
667
  let keep_ite = (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false) in
667
  let keep_ite = (match !Options.output with | "horn" | "C" -> true | "java" | _ -> false) in
668 668
  let m, init, j, locals, s = translate_eqs nd keep_ite [] init_args (List.rev sorted_eqs_rev) in
669 669
  let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
670 670
  {
......
684 684
	   common branches are not merged while they are in C or Java
685 685
	   backends. *)
686 686
	match !Options.output with
687
	| "horn" -> s
688
	| "C" | "java" | _ -> join_guards_list s
687
	| "C" | "horn" -> s
688
	| "java" | _ -> join_guards_list s
689 689
      );
690 690
    };
691 691
    mspec = Utils.option_map (translate_spec nd) nd.node_spec;

Also available in: Unified diff