diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-10-12 11:48:36 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-10-12 11:48:36 +0200 |
commit | 3ab947ce345e9d18ddcda57d8f88b2a9b8f5d267 (patch) | |
tree | 41afaa730849b6f9e8116ddc3068044928997d8c /configure | |
parent | ef0f69dc1caeab169dcefca4d8b89f4d9e756bb5 (diff) | |
download | compcert-3ab947ce345e9d18ddcda57d8f88b2a9b8f5d267.tar.gz compcert-3ab947ce345e9d18ddcda57d8f88b2a9b8f5d267.zip |
Removal of cchecklink, superseded by AbsInt's Valex tool.
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 32 |
1 files changed, 6 insertions, 26 deletions
@@ -19,17 +19,16 @@ toolprefix='' target='' has_runtime_lib=true has_standard_headers=true -build_checklink=true advanced_debug=false usage='Usage: ./configure [options] target Supported targets: - ppc-linux (PowerPC, Linux) ppc-eabi (PowerPC, EABI with GNU/Unix tools) ppc-eabi-diab (PowerPC, EABI with Diab tools) - arm-linux (ARM, EABI) + ppc-linux (PowerPC, Linux) arm-eabi (ARM, EABI) + arm-linux (ARM, EABI) arm-eabihf (ARM, EABI using hardware FP registers) arm-hardfloat (ARM, EABI using hardware FP registers) ia32-linux (x86 32 bits, Linux) @@ -40,7 +39,7 @@ Supported targets: For PowerPC targets, the "ppc-" prefix can be refined into: ppc64- PowerPC 64 bits - e5500- FreeCell e5500 core (PowerPC 64 bits + EREF extensions) + e5500- Freescale e5500 core (PowerPC 64 bits + EREF extensions) For ARM targets, the "arm-" prefix can be refined into: armv6- ARMv6 + VFPv2 @@ -74,8 +73,6 @@ while : ; do has_runtime_lib=false;; -no-standard-headers) has_standard_headers=false;; - -no-checklink) - build_checklink=false;; *) if test -n "$target"; then echo "$usage" 1>&2; exit 2; fi target="$1";; @@ -85,7 +82,6 @@ done # Per-target configuration -cchecklink=false casmruntime="" asm_supports_cfi="" struct_passing="" @@ -114,7 +110,6 @@ case "$target" in asm_supports_cfi=false clinker="${toolprefix}dcc" libmath="-lm" - cchecklink=${build_checklink} advanced_debug=true;; *) system="linux" @@ -124,7 +119,6 @@ case "$target" in casmruntime="${toolprefix}gcc -c -Wa,-mregnames" clinker="${toolprefix}gcc" libmath="-lm" - cchecklink=${build_checklink} advanced_debug=true;; esac;; arm*-*) @@ -326,20 +320,6 @@ if $missingtools; then exit 2 fi -# Additional packages needed for cchecklink - -if $cchecklink; then - echo "Testing availability of ocaml-bitstring... " | tr -d '\n' - if ocamlfind query bitstring > /dev/null - then - echo "yes" - else - echo "no" - echo "ocamlfind or ocaml-bitstring missing, cchecklink will not be built" - cchecklink=false - fi -fi - # Generate Makefile.config sharedir="$(dirname "$bindir")"/share @@ -369,7 +349,6 @@ CLINKER=$clinker LIBMATH=$libmath HAS_RUNTIME_LIB=$has_runtime_lib HAS_STANDARD_HEADERS=$has_standard_headers -CCHECKLINK=$cchecklink ASM_SUPPORTS_CFI=$asm_supports_cfi ADVANCED_DEBUG=$advanced_debug EOF @@ -383,7 +362,9 @@ cat >> Makefile.config <<'EOF' ARCH= # Hardware variant -# MODEL=standard # for PowerPC +# MODEL=ppc32 # for plain PowerPC +# MODEL=ppc64 # for PowerPC with 64-bit instructions +# MODEL=e5500 # for Freescale e5500 PowerPC variant # MODEL=armv6 # for ARM # MODEL=armv7a # for ARM # MODEL=armv7r # for ARM @@ -488,7 +469,6 @@ CompCert configuration: Library files installed in.... $libdirexp Standard headers provided..... $has_standard_headers Standard headers installed in. $libdirexp/include - cchecklink tool supported..... $cchecklink Build command to use.......... $make If anything above looks wrong, please edit file ./Makefile.config to correct. |