aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile12
1 files changed, 8 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index 24cfefd..ee111eb 100644
--- a/Makefile
+++ b/Makefile
@@ -8,17 +8,20 @@ endif
COMPCERTRECDIRS := lib common verilog backend cfrontend driver exportclight cparser
-COQINCLUDES := -R src/common vericert.common -R src/verilog vericert.verilog \
- -R src/extraction vericert.extraction -R src/translation vericert.translation \
+COQINCLUDES := -R src/common vericert.common \
+ -R src/extraction vericert.extraction \
+ -R src/hls vericert.hls \
-R src vericert \
- $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d))
+ $(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d)) \
+ -R lib/CompCert/flocq Flocq \
+ -R lib/CompCert/MenhirLib MenhirLib
COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
COQMAKE := $(COQBIN)coq_makefile
COQDOCFLAGS := --no-lib-name -l
-VS := src/Compiler.v src/Simulator.v $(foreach d, translation common verilog, src/$(d)/*.v)
+VS := src/Compiler.v src/Simulator.v $(foreach d, common hls, src/$(d)/*.v)
PREFIX ?= .
@@ -35,6 +38,7 @@ lib/COMPCERTSTAMP:
install:
install -d $(PREFIX)/bin
+ sed -i'' -e 's/arch=verilog/arch=x86/' _build/default/driver/compcert.ini
install -C _build/default/driver/compcert.ini $(PREFIX)/bin/.
install -C _build/default/driver/VericertDriver.exe $(PREFIX)/bin/vericert