Merge pull request #213 from AeneasVerif/cleanup-tests

1 files changed, 11 insertions, 34 deletions

diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 1c885d4b..c626b4d1 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -100,32 +100,6 @@ module Command = struct
     | Failure -> ()
 end
 
-let aeneas_options_for_test backend test_name =
-  if test_name = "betree" then
-    let options =
-      [
-        "-backward-no-state-update";
-        "-test-trans-units";
-        "-state";
-        "-split-files";
-      ]
-    in
-    let extra_options =
-      match backend with
-      | Backend.Coq -> [ "-use-fuel" ]
-      | Backend.FStar -> [ "-decreases-clauses"; "-template-clauses" ]
-      | _ -> []
-    in
-    List.append extra_options options
-  else []
-
-(* File-specific options *)
-let charon_options_for_test test_name =
-  match test_name with
-  | "betree" ->
-      [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
-  | _ -> []
-
 (* The data for a specific test input *)
 module Input = struct
   type kind = SingleFile | Crate
@@ -219,13 +193,10 @@ module Input = struct
       else failwith ("`" ^ path ^ "` is not a file or a directory.")
     in
     let actions = BackendMap.make (fun _ -> Normal) in
-    let charon_options = charon_options_for_test name in
     let subdirs =
       BackendMap.make (fun backend -> default_subdir backend name)
     in
-    let aeneas_options =
-      BackendMap.make (fun backend -> aeneas_options_for_test backend name)
-    in
+    let aeneas_options = BackendMap.make (fun _ -> []) in
     let check_output = BackendMap.make (fun _ -> true) in
     let input =
       {
@@ -233,12 +204,14 @@ module Input = struct
         name;
         kind;
         actions;
-        charon_options;
+        charon_options = [];
         subdirs;
         aeneas_options;
         check_output;
       }
     in
+    (* For crates, we store the special comments in a separate file. *)
+    let crate_config_file = Filename.concat path "aeneas-test-options" in
     match kind with
     | SingleFile ->
         let file_lines = Core.In_channel.read_lines path in
@@ -252,15 +225,18 @@ module Input = struct
         List.fold_left
           (fun input comment -> apply_special_comment comment input)
           input special_comments
+    | Crate when Sys.file_exists crate_config_file ->
+        let special_comments = Core.In_channel.read_lines crate_config_file in
+        List.fold_left
+          (fun input comment -> apply_special_comment comment input)
+          input special_comments
     | Crate -> input
 end
 
 (* Run Aeneas on a specific input with the given options *)
 let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
-  (* FIXME: remove this special case *)
   let backend_str = Backend.to_string backend in
-  let test_name = if case.name = "betree" then "betree_main" else case.name in
-  let input_file = concat_path [ env.llbc_dir; test_name ] ^ ".llbc" in
+  let input_file = concat_path [ env.llbc_dir; case.name ] ^ ".llbc" in
   let output_file =
     Filename.remove_extension case.path ^ "." ^ backend_str ^ ".out"
   in
@@ -303,6 +279,7 @@ let run_aeneas (env : runner_env) (case : Input.t) (backend : Backend.t) =
       let cmd = { cmd with redirect_out = Some out } in
       Command.run_command_expecting_failure cmd;
       Unix.close out
+
 (* Run Charon on a specific input with the given options *)
 let run_charon (env : runner_env) (case : Input.t) =
   match case.kind with