summaryrefslogtreecommitdiff
path: root/tests/test_runner
diff options
context:
space:
mode:
authorGuillaume Boisseau2024-05-28 11:56:39 +0200
committerGitHub2024-05-28 11:56:39 +0200
commitef7792c106a1f33397c206fcb5124b5ddfe64378 (patch)
treea72fae46702fc4c2eb32e1361a2538eb7a5f5545 /tests/test_runner
parent4f26c7f6f1e554d8ec2f46e868d5dc66c4160d16 (diff)
parentc4d2af051c18c4c81b1e57a45210c37c89c8330f (diff)
Merge pull request #213 from AeneasVerif/cleanup-tests
Diffstat (limited to 'tests/test_runner')
-rw-r--r--tests/test_runner/run_test.ml45
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