From 245de5902d72a2de43f488203942d1fb68430b4f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Mar 2023 12:39:21 +0100
Subject: Remove the symbolic interpreter tests

---
 compiler/Driver.ml      |  5 -----
 compiler/Interpreter.ml | 30 ------------------------------
 2 files changed, 35 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Driver.ml b/compiler/Driver.ml
index 476907c1..12a6f075 100644
--- a/compiler/Driver.ml
+++ b/compiler/Driver.ml
@@ -219,11 +219,6 @@ let () =
       (* Test the unit functions with the concrete interpreter *)
       if !test_unit_functions then I.Test.test_unit_functions m;
 
-      (* Evaluate the symbolic interpreter on the functions, ignoring the
-       * functions which contain loops - TODO: remove *)
-      let synthesize = true in
-      I.Test.test_functions_symbolic synthesize m;
-
       (* Translate the functions *)
       Translate.translate_crate filename dest_dir m;
 
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index a69b7b51..ccb9009e 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -549,34 +549,4 @@ module Test = struct
     in
 
     ()
-
-  (** Small helper *)
-  let fun_decl_is_transparent (def : A.fun_decl) : bool =
-    Option.is_some def.body
-
-  (** Execute the symbolic interpreter on a list of functions.
-
-      TODO: for now we ignore the functions which contain loops, because
-      they are not supported by the symbolic interpreter.
-   *)
-  let test_functions_symbolic (synthesize : bool) (crate : A.crate) : unit =
-    (* Filter the functions which contain loops *)
-    let no_loop_funs =
-      List.filter
-        (fun f -> not (LlbcAstUtils.fun_decl_has_loops f))
-        crate.functions
-    in
-    (* Filter the opaque functions *)
-    let no_loop_funs = List.filter fun_decl_is_transparent no_loop_funs in
-    let type_context, fun_context, global_context =
-      compute_type_fun_global_contexts crate
-    in
-    let test_fun (def : A.fun_decl) : unit =
-      (* Execute the function - note that as the symbolic interpreter explores
-       * all the path, some executions are expected to "panic": we thus don't
-       * check the return value *)
-      test_function_symbolic synthesize type_context fun_context global_context
-        def
-    in
-    List.iter test_fun no_loop_funs
 end
-- 
cgit v1.2.3