diff options
author | Nadrieril | 2024-05-22 19:23:03 +0200 |
---|---|---|
committer | Guillaume Boisseau | 2024-05-24 14:24:38 +0200 |
commit | a9471e615e03d6fa0bc1594176fe504c9a3c88ae (patch) | |
tree | 31ce18c2d053ecf40dcced79336df11a963bffbb /tests | |
parent | 6ae8cde046530371345863f04d84be32b2a757bf (diff) |
Set all options in the test runner
Diffstat (limited to '')
-rw-r--r-- | tests/test_runner/run_test.ml | 57 |
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" |