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)