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