summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile91
-rw-r--r--flake.lock7
-rw-r--r--flake.nix3
3 files changed, 23 insertions, 78 deletions
diff --git a/Makefile b/Makefile
index f4bb8f9e..414f562d 100644
--- a/Makefile
+++ b/Makefile
@@ -20,11 +20,6 @@ REGEN_LLBC ?=
# The path to Charon
CHARON_HOME ?= ../charon
-# The paths to the test directories in Charon (Aeneas will look for the .llbc
-# files in there).
-CHARON_TESTS_REGULAR_DIR ?= $(CHARON_HOME)/tests
-CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius
-
# The path to the Aeneas executable to run the tests - we need the ability to
# change this path for the Nix package.
AENEAS_EXE ?= bin/aeneas
@@ -36,7 +31,7 @@ OPTIONS ?=
# The rules use (and update) the following variables
#
# The Charon test directory where to look for the .llbc files
-CHARON_TEST_DIR =
+CHARON_TEST_DIR ?= $(CHARON_HOME)/tests
# The options with which to call Charon
CHARON_OPTIONS =
# The backend sub-directory in which to generate the files
@@ -94,8 +89,8 @@ test: build-dev test-all
test-all: test-no_nested_borrows test-paper \
test-hashmap test-hashmap_main \
test-external test-constants \
- test-polonius_list testp-betree_main \
- ctest-testp-betree_main \
+ test-polonius_list test-betree_main \
+ ctest-test-betree_main \
test-loops \
test-arrays test-traits test-bitwise test-demo
@@ -220,97 +215,57 @@ thol4-bitwise: SUBDIR := misc-bitwise
thol4-bitwise: OPTIONS +=
BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
-testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
-testp-betree_main: SUBDIR:=betree
-tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
-tcoqp-betree_main: OPTIONS += -use-fuel
-tleanp-betree_main: SUBDIR :=
-tleanp-betree_main: OPTIONS +=
+test-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
+test-betree_main: SUBDIR:=betree
+tfstar-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
+tcoq-betree_main: OPTIONS += -use-fuel
+tlean-betree_main: SUBDIR :=
+tlean-betree_main: OPTIONS +=
thol4-betree_main: OPTIONS +=
# Additional, *c*ustom test on the betree: translate it without `-backward-no-state-update`.
# This generates very ugly code, but is good to test the translation.
-.PHONY: ctest-testp-betree_main
-ctest-testp-betree_main: testp-betree_main
-ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units -state -split-files
-ctest-testp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
-ctest-testp-betree_main: BACKEND_SUBDIR := "fstar"
-ctest-testp-betree_main: SUBDIR:=betree_back_stateful
-ctest-testp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-ctest-testp-betree_main: FILE = betree_main
-ctest-testp-betree_main:
+.PHONY: ctest-test-betree_main
+ctest-test-betree_main: test-betree_main
+ctest-test-betree_main: OPTIONS += -backend fstar -test-trans-units -state -split-files
+ctest-test-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
+ctest-test-betree_main: BACKEND_SUBDIR := "fstar"
+ctest-test-betree_main: SUBDIR:=betree_back_stateful
+ctest-test-betree_main: FILE = betree_main
+ctest-test-betree_main:
$(AENEAS_CMD)
# Generic rules to extract the LLBC from a rust file
# We use the rules in Charon's Makefile to generate the .llbc files: the options
# vary with the test files.
.PHONY: gen-llbc-%
-gen-llbc-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
gen-llbc-%:
$(CHARON_CMD)
-# "p" stands for "Polonius"
-.PHONY: gen-llbcp-%
-gen-llbcp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-gen-llbcp-%:
- $(CHARON_CMD)
-
-# Generic rules to test the testlation of an LLBC file.
-# Note that the files requiring the Polonius borrow-checker are generated
-# in the tests-polonius subdirectory.
+# Generic rules to test the translation of an LLBC file.
.PHONY: test-%
-test-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
test-%: FILE = $*
test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-%
echo "# Test $* done"
-# "p" stands for "Polonius"
-.PHONY: testp-%
-testp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-testp-%: FILE = $*
-testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
- echo "# Test $* done"
-
.PHONY: tfstar-%
tfstar-%: OPTIONS += -backend fstar
tfstar-%: BACKEND_SUBDIR := fstar
tfstar-%:
$(AENEAS_CMD)
-# "p" stands for "Polonius"
-.PHONY: tfstarp-%
-tfstarp-%: OPTIONS += -backend fstar
-tfstarp-%: BACKEND_SUBDIR := fstar
-tfstarp-%:
- $(AENEAS_CMD)
-
.PHONY: tcoq-%
tcoq-%: OPTIONS += -backend coq
tcoq-%: BACKEND_SUBDIR := coq
tcoq-%:
$(AENEAS_CMD)
-# "p" stands for "Polonius"
-.PHONY: tcoqp-%
-tcoqp-%: OPTIONS += -backend coq
-tcoqp-%: BACKEND_SUBDIR := coq
-tcoqp-%:
- $(AENEAS_CMD)
-
.PHONY: tlean-%
tlean-%: OPTIONS += -backend lean
tlean-%: BACKEND_SUBDIR := lean
tlean-%:
$(AENEAS_CMD)
-# "p" stands for "Polonius"
-.PHONY: tleanp-%
-
-tleanp-%: OPTIONS += -backend lean
-tleanp-%: BACKEND_SUBDIR := lean
-tleanp-%:
- $(AENEAS_CMD)
-
# TODO: reactivate HOL4 once traits are parameterized by their associated types
.PHONY: thol4-%
thol4-%: OPTIONS += -backend hol4
@@ -321,16 +276,6 @@ thol4-%:
#thol4-%:
# $(AENEAS_CMD)
-# TODO: reactivate HOL4 once traits are parameterized by their associated types
-.PHONY: thol4p-%
-thol4p-%: OPTIONS += -backend hol4
-thol4p-%: BACKEND_SUBDIR := hol4
-thol4p-%:
- echo Ignoring the $* test for HOL4
-
-#thol4p-%:
-# $(AENEAS_CMD)
-
# Nix - TODO: add the lean tests
.PHONY: nix
nix:
diff --git a/flake.lock b/flake.lock
index 014b0af1..e901898b 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,15 +9,16 @@
"rust-overlay": "rust-overlay"
},
"locked": {
- "lastModified": 1714483898,
- "narHash": "sha256-R9c3HgcKZQq6VF7ZBjidiJTtxB2mYNJYxctD1JI7As0=",
+ "lastModified": 1714656338,
+ "narHash": "sha256-+ksk7i8Kzm1V1rR/auH2EGlzGefPYgiuWMfAEH1Efjk=",
"owner": "aeneasverif",
"repo": "charon",
- "rev": "eb48f4a62ce7c330d44c1e3c870b2a7271bba73b",
+ "rev": "c54e6dc374fd77b0da8328f34f17a5b44e8d6ed0",
"type": "github"
},
"original": {
"owner": "aeneasverif",
+ "ref": "main",
"repo": "charon",
"type": "github"
}
diff --git a/flake.nix b/flake.nix
index 6f868e3b..fd94d1d0 100644
--- a/flake.nix
+++ b/flake.nix
@@ -85,8 +85,7 @@
};
buildPhase = ''
# We need to provide the paths to the Charon tests derivations
- export CHARON_TESTS_REGULAR_DIR=${charon.checks.${system}.tests}
- export CHARON_TESTS_POLONIUS_DIR=${charon.checks.${system}.tests-polonius}
+ export CHARON_TEST_DIR=${charon.checks.${system}.tests}
# Copy the Aeneas executable, and update the path to it
cp ${aeneas}/bin/aeneas aeneas