diff options
Diffstat (limited to 'scheduling/RTLtoBTLaux.ml')
| -rw-r--r-- | scheduling/RTLtoBTLaux.ml | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml new file mode 100644 index 00000000..8ace6e2a --- /dev/null +++ b/scheduling/RTLtoBTLaux.ml @@ -0,0 +1,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) |