summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2023-03-07 12:39:21 +0100
committerSon HO2023-06-04 21:44:33 +0200
commit245de5902d72a2de43f488203942d1fb68430b4f (patch)
tree9ae9975cd34aaea03a1d99cab9d088a401cec937 /compiler
parent72c824f3d93a737b9b8a51fa6a7c3060d2d40597 (diff)
Remove the symbolic interpreter tests
Diffstat (limited to '')
-rw-r--r--compiler/Driver.ml5
-rw-r--r--compiler/Interpreter.ml30
2 files changed, 0 insertions, 35 deletions
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