Revision df647a81 src/machine_code.ml
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