diff options
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 69 |
1 files changed, 45 insertions, 24 deletions
@@ -43,6 +43,8 @@ Supported targets: x86_32-cygwin (x86 32 bits, Cygwin environment under Windows) x86_64-linux (x86 64 bits, Linux) x86_64-macosx (x86 64 bits, MacOS X) + rv32-linux (RISC-V 32 bits, Linux) + rv64-linux (RISC-V 64 bits, Linux) manual (edit configuration file by hand) For x86 targets, the "x86_32-" prefix can also be written "ia32-". @@ -52,12 +54,14 @@ For PowerPC targets, the "ppc-" prefix can be refined into: e5500- Freescale e5500 core (PowerPC 64 bit, EREF extensions) For ARM targets, the "arm-" or "armeb-" prefix can be refined into: - armv6- ARMv6 + VFPv2 + armv6- ARMv6 + VFPv2 (Thumb mode not supported) + armv6t2- ARMv6T2 + VFPv2 armv7a- ARMv7-A + VFPv3-d16 (default for arm-) armv7r- ARMv7-R + VFPv3-d16 armv7m- ARMv7-M + VFPv3-d16 - armebv6- ARMv6 + VFPv2 + armebv6- ARMv6 + VFPv2 (Thumb mode not supported) + armebv6t2- ARMv6T2 + VFPv2 armebv7a- ARMv7-A + VFPv3-d16 (default for armeb-) armebv7r- ARMv7-R + VFPv3-d16 armebv7m- ARMv7-M + VFPv3-d16 @@ -113,6 +117,8 @@ case "$target" in arch="arm"; model="armv7a"; endianness="little"; bitsize=32;; armv6-*) arch="arm"; model="armv6"; endianness="little"; bitsize=32;; + armv6t2-*) + arch="arm"; model="armv6t2"; endianness="little"; bitsize=32;; armv7r-*) arch="arm"; model="armv7r"; endianness="little"; bitsize=32;; armv7m-*) @@ -121,6 +127,8 @@ case "$target" in arch="arm"; model="armv7a"; endianness="big"; bitsize=32;; armebv6-*) arch="arm"; model="armv6"; endianness="big"; bitsize=32;; + armebv6t2-*) + arch="arm"; model="armv6t2"; endianness="big"; bitsize=32;; armebv7r-*) arch="arm"; model="armv7r"; endianness="big"; bitsize=32;; armebv7m-*) @@ -157,10 +165,10 @@ target=${target#[a-zA-Z0-9]*-} # Per-target configuration -clinker_needs_no_pie=true asm_supports_cfi="" casm_options="" casmruntime="" +clinker_needs_no_pie=true clinker_options="" cprepro_options="" struct_passing="" @@ -282,7 +290,7 @@ if test "$arch" = "x86" -a "$bitsize" = "32"; then clinker="${toolprefix}gcc" clinker_options="-m32" cprepro="${toolprefix}gcc" - cprepro_options="-std=c99 -m32 -U__GNUC__ -E" + cprepro_options="-std=c99 -m32 -U__GNUC__ '-D__attribute__(x)=' -E" libmath="-lm" struct_passing="ints" struct_return="ref" @@ -378,6 +386,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then esac fi + # # RISC-V Target Configuration # @@ -401,20 +410,39 @@ if test "$arch" = "riscV"; then system="linux" fi + # # Finalize Target Configuration # if test -z "$casmruntime"; then casmruntime="$casm $casm_options"; fi +# Invoke a C compiler, e.g. to check for availability of command-line options +testcompiler () { + tmpsrc="${TMPDIR:-/tmp}/compcert-configure-$$.c" + rm -f "$tmpsrc" + tmpout="${TMPDIR:-/tmp}/compcert-configure-$$.out" + rm -f "$tmpout" + cat >> "$tmpsrc" <<EOF +int main (void) +{ + return 0; +} +EOF + "$@" -o "$tmpout" "$tmpsrc" >/dev/null 2>/dev/null + retcode=$? + rm -f "$tmpsrc" "$tmpout" + return $retcode +} + # # Test Assembler Support for CFI Directives # if test "$target" != "manual" && test -z "$asm_supports_cfi"; then echo "Testing assembler support for CFI directives... " | tr -d '\n' - f=/tmp/compcert-configure-$$.s - rm -f $f - cat >> $f <<EOF + tmpsrc="${TMPDIR:-/tmp}/compcert-configure-$$.s" + rm -f "$tmpsrc" + cat >> "$tmpsrc" <<EOF testfun: .file 1 "testfun.c" .loc 1 1 @@ -422,11 +450,11 @@ testfun: .cfi_adjust_cfa_offset 16 .cfi_endproc EOF - if $casm $casm_options -o /dev/null $f 2>/dev/null + if $casm $casm_options -o /dev/null "$tmpsrc" 2>/dev/null then echo "yes"; asm_supports_cfi=true else echo "no"; asm_supports_cfi=false fi - rm -f $f + rm -f "$tmpsrc" fi @@ -435,23 +463,10 @@ fi # if ($clinker_needs_no_pie) then echo "Testing linker support for '-no-pie' option... " | tr -d '\n' - fx=/tmp/compcert-configure-$$.elf - rm -f $fx - f=/tmp/compcert-configure-$$.c - rm -f $f - cat >> $f <<EOF -int main (void) -{ - return 0; -} -EOF - $cc -no-pie -o $fx $f >/dev/null 2>&1 - status=$? - if [ $status -eq 0 ] + if testcompiler ${cc} -no-pie; then echo "yes"; clinker_options="${clinker_options} -no-pie" else echo "no"; clinker_needs_no_pie=false fi - rm -f $f $fx fi @@ -463,7 +478,7 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.6) + 8.6|8.6.1) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" @@ -486,6 +501,11 @@ case "$ocaml_ver" in echo "version $ocaml_ver -- UNSUPPORTED" echo "Error: CompCert requires OCaml version 4.02 or later." missingtools=true;; + 4.02.*|4.03.*|4.04.*) + echo "version $ocaml_ver -- good!" + echo "WARNING: some Intel processors of the Skylake and Kaby Lake generations" + echo "have a hardware bug that can be triggered by this version of OCaml." + echo "To avoid this risk, it is recommended to use OCaml 4.05.";; 4.0*) echo "version $ocaml_ver -- good!";; ?.*) @@ -649,6 +669,7 @@ ARCH= # MODEL=ppc64 # for PowerPC with 64-bit instructions # MODEL=e5500 # for Freescale e5500 PowerPC variant # MODEL=armv6 # for ARM +# MODEL=armv6t2 # for ARM # MODEL=armv7a # for ARM # MODEL=armv7r # for ARM # MODEL=armv7m # for ARM |