diff options
| -rw-r--r-- | tests/src/betree/aeneas-test-options | 4 | ||||
| -rw-r--r-- | tests/test_runner/run_test.ml | 40 |
2 files changed, 14 insertions, 30 deletions
diff --git a/tests/src/betree/aeneas-test-options b/tests/src/betree/aeneas-test-options new file mode 100644 index 00000000..c71e01df --- /dev/null +++ b/tests/src/betree/aeneas-test-options @@ -0,0 +1,4 @@ +charon-args=--polonius --opaque=betree_utils +aeneas-args=-backward-no-state-update -test-trans-units -state -split-files +[coq] aeneas-args=-use-fuel +[fstar] aeneas-args=-decreases-clauses -template-clauses diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml index a7b83e88..c626b4d1 100644 --- a/tests/test_runner/run_test.ml +++ b/tests/test_runner/run_test.ml @@ -100,31 +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" ] - | _ -> [] - (* The data for a specific test input *) module Input = struct type kind = SingleFile | Crate @@ -218,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 = { @@ -232,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 @@ -251,6 +225,11 @@ 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 @@ -300,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 |