aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-04-25 12:38:16 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-04-25 12:38:16 +0200
commit1909a882df9e40c079b7fbcdfba3d1742c52a0fb (patch)
tree3649a07f7fb56bd9f1d05e7a65b3a30fc807c75d /Makefile
parent3c6f5343e0e64b273658b6b3508a8dd6c29b8cef (diff)
downloadcompcert-kvx-1909a882df9e40c079b7fbcdfba3d1742c52a0fb.tar.gz
compcert-kvx-1909a882df9e40c079b7fbcdfba3d1742c52a0fb.zip
Provide and use compiler-dependent standard headers.
This branch provides implementations of the following standard headers: <float.h> <stdarg.h> <stdbool.h> <stddef.h> <varargs.h> These are the headers that are provided by GCC and Clang, as opposed to being provided by Glibc and similar C standard libraries. Configuration flag "-no-standard-headers" deactivates the installation and use of these headers. Lightly tested so far (IA32 Linux).
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile9
1 files changed, 4 insertions, 5 deletions
diff --git a/Makefile b/Makefile
index afd26c4c..2205ed64 100644
--- a/Makefile
+++ b/Makefile
@@ -202,6 +202,7 @@ compcert.ini: Makefile.config VERSION
echo "abi=$(ABI)"; \
echo "system=$(SYSTEM)"; \
echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \
+ echo "has_standard_headers=$(HAS_STANDARD_HEADERS)"; \
echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \
echo "advanced_debug=$(ADVANCED_DEBUG)"; \
echo "struct_passing_style=$(STRUCT_PASSING)"; \
@@ -220,15 +221,13 @@ depend: $(FILES) exportclight/Clightdefs.v
install:
install -d $(BINDIR)
- install ./ccomp $(BINDIR)
+ install -m 0755 ./ccomp $(BINDIR)
install -d $(SHAREDIR)
- install ./compcert.ini $(SHAREDIR)
+ install -m 0644 ./compcert.ini $(SHAREDIR)
ifeq ($(CCHECKLINK),true)
- install ./cchecklink $(BINDIR)
+ install -m 0755 ./cchecklink $(BINDIR)
endif
-ifeq ($(HAS_RUNTIME_LIB),true)
$(MAKE) -C runtime install
-endif
clean:
rm -f $(patsubst %, %/*.vo, $(DIRS))