aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--Makefile16
-rwxr-xr-xconfigure8
2 files changed, 14 insertions, 10 deletions
diff --git a/Makefile b/Makefile
index 1bf53bff..b7b99e46 100644
--- a/Makefile
+++ b/Makefile
@@ -123,10 +123,11 @@ all:
ifeq ($(HAS_RUNTIME_LIB),true)
$(MAKE) runtime
endif
-ifeq ($(CCHECKLINK),true)
- $(MAKE) cchecklink
+ifeq ($(CLIGHTGEN),true)
+ $(MAKE) clightgen
endif
+
proof: $(FILES:.v=.vo)
extraction: extraction/STAMP
@@ -144,11 +145,6 @@ ccomp: .depend.extr compcert.ini driver/Version.ml FORCE
ccomp.byte: .depend.extr compcert.ini driver/Version.ml FORCE
$(MAKE) -f Makefile.extr ccomp.byte
-cchecklink: .depend.extr compcert.ini driver/Version.ml FORCE
- $(MAKE) -f Makefile.extr cchecklink
-cchecklink.byte: .depend.extr compcert.ini driver/Version.ml FORCE
- $(MAKE) -f Makefile.extr cchecklink.byte
-
clightgen: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE
$(MAKE) -f Makefile.extr clightgen
clightgen.byte: .depend.extr compcert.ini exportclight/Clightdefs.vo driver/Version.ml FORCE
@@ -228,10 +224,10 @@ install:
install -m 0755 ./ccomp $(BINDIR)
install -d $(SHAREDIR)
install -m 0644 ./compcert.ini $(SHAREDIR)
-ifeq ($(CCHECKLINK),true)
- install -m 0755 ./cchecklink $(BINDIR)
-endif
$(MAKE) -C runtime install
+ifeq ($(CLIGHTGEN),true)
+ install -m 0755 ./clightgen $(BINDIR)
+endif
clean:
rm -f $(patsubst %, %/*.vo, $(DIRS))
diff --git a/configure b/configure
index 21aa5c75..81c1a6fd 100755
--- a/configure
+++ b/configure
@@ -20,6 +20,7 @@ target=''
has_runtime_lib=true
has_standard_headers=true
advanced_debug=false
+clightgen=false
usage='Usage: ./configure [options] target
@@ -54,6 +55,7 @@ Options:
-toolprefix <pref> Prefix names of tools ("gcc", etc) with <pref>
-no-runtime-lib Do not compile nor install the runtime support library
-no-standard-headers Do not install nor use the standard .h headers
+ -clightgen Also compile the clightgen tool
'
# Parse command-line arguments
@@ -73,6 +75,8 @@ while : ; do
has_runtime_lib=false;;
-no-standard-headers)
has_standard_headers=false;;
+ -clightgen)
+ clightgen=true;;
*)
if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi
target="$1";;
@@ -352,6 +356,7 @@ HAS_RUNTIME_LIB=$has_runtime_lib
HAS_STANDARD_HEADERS=$has_standard_headers
ASM_SUPPORTS_CFI=$asm_supports_cfi
ADVANCED_DEBUG=$advanced_debug
+CLIGHTGEN=$clightgen
EOF
else
cat >> Makefile.config <<'EOF'
@@ -432,6 +437,9 @@ HAS_STANDARD_HEADERS=true
ASM_SUPPORTS_CFI=false
#ASM_SUPPORTS_CFI=true
+# Turn on/off compilation of clightgen
+CLIGHTGEN=false
+
EOF
fi