diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-28 21:31:24 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-28 21:31:24 +0100 |
commit | 69d6a2c1e08e6169af95bf895d6b0380edb0d081 (patch) | |
tree | 38ff4dc08878b1f005e4c12c5dfede83e2e04d45 | |
parent | 070adbfa6fbddee552e689bbee4bf76fa4bf770a (diff) | |
download | compcert-69d6a2c1e08e6169af95bf895d6b0380edb0d081.tar.gz compcert-69d6a2c1e08e6169af95bf895d6b0380edb0d081.zip |
Added configuration to enable clightgen build.
The new configuration option -clightgen activates the build of clightgen.
-rw-r--r-- | Makefile | 16 | ||||
-rwxr-xr-x | configure | 8 |
2 files changed, 14 insertions, 10 deletions
@@ -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)) @@ -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 |