1 files changed, 18 insertions, 8 deletions
diff --git a/src/Translate.ml b/src/Translate.ml
index 8c6a6def..efdad619 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -3,6 +3,7 @@ module T = Types
 module A = CfimAst
 module M = Modules
 module SA = SymbolicAst
+open Errors
 open Cps
 open InterpreterUtils
 open InterpreterStatements
@@ -10,18 +11,21 @@ open InterpreterStatements
 (** The local logger *)
 let log = L.translate_log
 
-(** Execute the symbolic interpreter on a function to generate a pure AST.
-    
-    We don't apply any micro pass.
- *)
-let translate_function_to_pure (config : C.partial_config) (m : M.cfim_module)
-    (fid : A.FunDefId.id) : unit =
+(** Execute the symbolic interpreter on a function to generate a symbolic AST. *)
+let translate_function_to_symbolic (config : C.partial_config)
+    (m : M.cfim_module) (fid : A.FunDefId.id)
+    (back_id : T.RegionGroupId.id option) : unit =
   (* Retrieve the function declaration *)
   let fdef = A.FunDefId.nth m.functions fid in
 
   (* Debug *)
   log#ldebug
-    (lazy ("translate_function_to_pure: " ^ Print.name_to_string fdef.A.name));
+    (lazy
+      ("translate_function_to_pure: "
+      ^ Print.name_to_string fdef.A.name
+      ^ " ("
+      ^ Print.option_to_string T.RegionGroupId.to_string back_id
+      ^ ")"));
 
   (* Create the evaluation context *)
   let ctx = initialize_symbolic_context_for_fun m fdef in
@@ -29,7 +33,7 @@ let translate_function_to_pure (config : C.partial_config) (m : M.cfim_module)
   (* Create the continuation to check the function's result *)
   let cf_check res _ =
     match res with
-    | Return -> if synthesize then raise Errors.Unimplemented else None
+    | Return -> raise Errors.Unimplemented
     | Panic ->
         (* Note that as we explore all the execution branches, one of
          * the executions can lead to a panic *)
@@ -44,3 +48,9 @@ let translate_function_to_pure (config : C.partial_config) (m : M.cfim_module)
   let config = C.config_of_partial C.SymbolicMode config in
   let _ = eval_function_body config fdef.A.body cf_check ctx in
   ()
+
+let translate (config : C.partial_config) (m : M.cfim_module) : unit =
+  (* Translate all the type definitions *)
+
+  (* Translate all the function signatures *)
+  raise Unimplemented