summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorSon Ho2022-02-23 22:23:45 +0100
committerSon Ho2022-02-23 22:23:45 +0100
commite3430dcb5e944af0903b272669e6ddbb8e7d59c3 (patch)
treeb538fc2151d7a7fb01b94ef9a5c7b29925f3c1c0 /Makefile
parent284a6042ca9d5d7bcbc19a10909156769443c9be (diff)
Add an option to control the translation to error monad or state-error
monad
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile19
1 files changed, 10 insertions, 9 deletions
diff --git a/Makefile b/Makefile
index cdae532d..53382164 100644
--- a/Makefile
+++ b/Makefile
@@ -1,10 +1,10 @@
all: build-test
-CHARON_HOME=../charon
-CHARON_EXEC=$(CHARON_HOME)/charon
-CHARON_TESTS_DIR=$(CHARON_HOME)/tests/cfim
-CHARON_OPTIONS= --dest ../tests/cfim --no-code-duplication
-DEST_DIR=tests
+CHARON_HOME = ../charon
+CHARON_EXEC = $(CHARON_HOME)/charon
+CHARON_TESTS_DIR = $(CHARON_HOME)/tests/cfim
+CHARON_OPTIONS = --dest ../tests/cfim --no-code-duplication
+DEST_DIR = tests
# The user can specify additional translation options for Aeneas:
OPTIONS ?=
@@ -12,8 +12,8 @@ OPTIONS ?=
# Default translation options:
# - insert calls to the normalizer in the translated code to test the
# generated unit functions
-TRANS_OPTIONS:=-test-trans-units $(OPTIONS)
-SUBDIR:=
+TRANS_OPTIONS := -test-trans-units $(OPTIONS)
+SUBDIR :=
# Build the project and test it
.PHONY: build-test
@@ -29,9 +29,10 @@ build:
test: build translate-no_nested_borrows translate-hashmap translate-paper
# Add specific options to some tests
-translate-no_nested_borrows translate-paper: TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split -no-decreases-clauses
+translate-no_nested_borrows translate-paper: \
+ TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split-files -no-decreases-clauses
translate-no_nested_borrows translate-paper: SUBDIR:=misc
-translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses
+translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses -no-state
translate-hashmap: SUBDIR:=hashmap
# Generic rule to extract the CFIM from a rust file