summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorSon Ho2022-10-26 17:31:24 +0200
committerSon HO2022-10-26 19:45:09 +0200
commite1f79b07440f35e5e6296b61819cf50e6f60f090 (patch)
tree88e7120146b7addd8cd83443d1aaea03beebacbb /Makefile
parent7d6e7a5608327d24bf8574bda53dc031d3b91140 (diff)
Start generating documentation
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile17
1 files changed, 13 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index c59aec01..3b822802 100644
--- a/Makefile
+++ b/Makefile
@@ -14,6 +14,8 @@ CHARON_TESTS_DIR =
CHARON_OPTIONS =
CHARON_TESTS_SRC =
+AENEAS_DRIVER = src/driver.exe
+
# The user can specify additional translation options for Aeneas:
OPTIONS ?=
@@ -29,8 +31,15 @@ build-tests-verify: build tests verify
# Build the project
.PHONY: build
-build:
- dune build src/main.exe
+build: build-driver build-lib
+
+.PHONY: build-driver
+build-driver:
+ dune build $(AENEAS_DRIVER)
+
+.PHONY: build-lib
+build-lib:
+ dune build src/aeneas.cmxs
# Test the project by translating test files to F*
.PHONY: tests
@@ -91,10 +100,10 @@ trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc
trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
trans-polonius-%: gen-llbc-polonius-%
- dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
+ dune exec -- $(AENEAS_DRIVER) $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
trans-%: gen-llbc-%
- dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
+ dune exec -- $(AENEAS_DRIVER) $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
.PHONY: doc
doc: