summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorNadrieril2024-05-22 19:23:03 +0200
committerGuillaume Boisseau2024-05-24 14:24:38 +0200
commita9471e615e03d6fa0bc1594176fe504c9a3c88ae (patch)
tree31ce18c2d053ecf40dcced79336df11a963bffbb /tests
parent6ae8cde046530371345863f04d84be32b2a757bf (diff)
Set all options in the test runner
Diffstat (limited to '')
-rw-r--r--tests/test_runner/run_test.ml57
1 files changed, 57 insertions, 0 deletions
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 52ff7276..949d5307 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -21,6 +21,63 @@ let () =
| _ -> test_name
in
+ (* File-specific options *)
+ (* TODO: reactivate -test-trans-units for hashmap and hashmap_main *)
+ let use_fuel =
+ match (backend, test_name) with
+ | ( "coq",
+ ( "arrays" | "betree_main" | "demo" | "hashmap" | "hashmap_main"
+ | "loops" ) ) ->
+ true
+ | "fstar", "demo" -> true
+ | _ -> false
+ in
+ let options = if use_fuel then "-use-fuel" :: options else options in
+
+ let decrease_template_clauses =
+ backend = "fstar"
+ &&
+ match test_name with
+ | "arrays" | "betree_main" | "betree_main-special" | "hashmap"
+ | "hashmap_main" | "loops" | "traits" ->
+ true
+ | _ -> false
+ in
+ let options =
+ if decrease_template_clauses then
+ "-decreases-clauses" :: "-template-clauses" :: options
+ else options
+ in
+
+ let extra_options =
+ match (backend, test_name) with
+ (* Additional, custom test on the betree: translate it without `-backward-no-state-update`. *)
+ (* This generates very ugly code, but is good to test the translation. *)
+ | _, "betree_main-special" ->
+ [ "-test-trans-units"; "-state"; "-split-files" ]
+ | _, "betree_main" ->
+ [
+ "-backward-no-state-update";
+ "-test-trans-units";
+ "-state";
+ "-split-files";
+ ]
+ | _, "bitwise" -> [ "-test-trans-units" ]
+ | _, "constants" -> [ "-test-trans-units" ]
+ | _, "external" -> [ "-test-trans-units"; "-state"; "-split-files" ]
+ | _, "hashmap_main" -> [ "-state"; "-split-files" ]
+ | _, "no_nested_borrows" -> [ "-test-trans-units" ]
+ | _, "paper" -> [ "-test-trans-units" ]
+ | _, "polonius_list" -> [ "-test-trans-units" ]
+ | "fstar", "arrays" -> [ "-split-files" ]
+ | "fstar", "loops" -> [ "-split-files" ]
+ (* We add a custom import in the Hashmap.lean file: we do not want to overwrite it *)
+ | "lean", "hashmap" -> [ "-split-files"; "-no-gen-lib-entry" ]
+ | _, "hashmap" -> [ "-split-files" ]
+ | _ -> []
+ in
+ let options = List.append extra_options options in
+
let test_file_name =
match test_name with
| "betree_main-special" -> "betree_main"