diff options
| author | Son Ho | 2022-11-11 16:05:56 +0100 |
|---|---|---|
| committer | Son Ho | 2022-11-11 16:05:56 +0100 |
| commit | b6676f6dc3b1471317cce8e04e9cb7203168f75c (patch) | |
| tree | 29954f1730a9bf2a4dfda30f32c7291383815a67 /Makefile | |
| parent | 61740913f8af53f0c1054375482b980ccb12f089 (diff) | |
Make minor modifications to the tests and regenerate the .fst files
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -86,7 +86,7 @@ clean: tests: trans-no_nested_borrows trans-paper \ trans-hashmap trans-hashmap_main \ trans-external trans-constants \ - trans-polonius-betree_polonius trans-polonius-betree_main \ + trans-polonius-polonius_list trans-polonius-betree_main \ test-trans-polonius-betree_main # Verify the F* files generated by the translation @@ -106,7 +106,7 @@ CHARON_CMD = cd $(CHARON_TEST_DIR) && NOT_ALL_TESTS=1 $(MAKE) test-$* endif # The command to run Aeneas on the proper llbc file -AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest ../tests/$(SUBDIR) $(OPTIONS) +AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(SUBDIR) $(OPTIONS) # Add specific options to some tests @@ -120,8 +120,8 @@ trans-hashmap: SUBDIR:=hashmap trans-hashmap_main: OPTIONS += -template-clauses trans-hashmap_main: SUBDIR:=hashmap_on_disk -trans-polonius-betree_polonius: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses -trans-polonius-betree_polonius: SUBDIR:=misc +trans-polonius-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses +trans-polonius-polonius_list: SUBDIR:=misc trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses trans-constants: SUBDIR:=misc |