blob: 8ace6e2ac8787ac32d2e78c9350804d569b4411e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
open RTLpathLivegenaux
open Maps
open RTL
open BinNums
open DebugPrint
let rtl2btl (f: RTL.coq_function) =
let code = f.fn_code in
let entry = f.fn_entrypoint in
let join_points = get_join_points code entry in
Printf.eprintf "test";
debug_flag := true;
debug "Join points: ";
print_true_nodes join_points;
debug "\n";
debug_flag := false;
((PTree.empty, Coq_xH), PTree.empty)
|
