From 5148617b7961c1d67acb70bfc783bc5616537486 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 5 Aug 2019 16:05:53 +0200
Subject: Add support for Coq 8.10

---
 configure | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'configure')

diff --git a/configure b/configure
index d586436a..9a2db366 100755
--- a/configure
+++ b/configure
@@ -503,14 +503,14 @@ 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.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1)
+  8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
         if $ignore_coq_version; then
             echo "Warning: this version of Coq is unsupported, proceed at your own risks."
         else
-            echo "Error: CompCert requires one of the following Coq versions: 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0"
+            echo "Error: CompCert requires one of the following Coq versions: 8.10, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0"
             missingtools=true
         fi;;
   "")
-- 
cgit 


From 7cdd676d002e33015b496f609538a9e86d77c543 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu, 8 Aug 2019 11:18:38 +0200
Subject: AArch64 port

This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
---
 configure | 38 ++++++++++++++++++++++++++++++++++----
 1 file changed, 34 insertions(+), 4 deletions(-)

(limited to 'configure')

diff --git a/configure b/configure
index 9a2db366..dccf6d14 100755
--- a/configure
+++ b/configure
@@ -55,10 +55,12 @@ Supported targets:
   x86_64-macosx        (x86 64 bits, MacOS X)
   rv32-linux           (RISC-V 32 bits, Linux)
   rv64-linux           (RISC-V 64 bits, Linux)
+  aarch64-linux        (AArch64, i.e. ARMv8 in 64-bit mode, Linux)
   manual               (edit configuration file by hand)
 
 For x86 targets, the "x86_32-" prefix can also be written "ia32-" or "i386-".
 For x86 targets, the "x86_64-" prefix can also be written "amd64-".
+For AArch64 targets, the "aarch64-" prefix can also be written "arm64-".
 
 For PowerPC targets, the "ppc-" prefix can be refined into:
   ppc64-               PowerPC 64 bits
@@ -175,6 +177,8 @@ case "$target" in
       arch="riscV"; model="32"; endianness="little"; bitsize=32;;
   rv64-*)
       arch="riscV"; model="64"; endianness="little"; bitsize=64;;
+  aarch64-*|arm64-*)
+      arch="aarch64"; model="default"; endianness="little"; bitsize=64;;
   manual)
       ;;
   "")
@@ -428,6 +432,29 @@ if test "$arch" = "riscV"; then
   system="linux"
 fi
 
+#
+# AArch64 (ARMv8 64 bits) Target Configuration
+#
+if test "$arch" = "aarch64"; then
+  case "$target" in
+    linux)
+        abi="standard"
+        casm="${toolprefix}gcc"
+        casm_options="-c"
+        cc="${toolprefix}gcc"
+        clinker="${toolprefix}gcc"
+        clinker_options=""
+        cprepro="${toolprefix}gcc"
+        cprepro_options="-std=c99 -U__GNUC__ -E"
+        libmath="-lm"
+        system="linux";;
+    *)
+        echo "Error: invalid eabi/system '$target' for architecture AArch64." 1>&2
+        echo "$usage" 1>&2
+        exit 2;;
+  esac
+fi
+
 
 #
 # Finalize Target Configuration
@@ -690,6 +717,8 @@ cat >> Makefile.config <<'EOF'
 # ARCH=powerpc
 # ARCH=arm
 # ARCH=x86
+# ARCH=riscV
+# ARCH=aarch6
 ARCH=
 
 # Hardware variant
@@ -703,23 +732,24 @@ ARCH=
 # MODEL=armv7m      # for ARM
 # MODEL=32sse2      # for x86 in 32-bit mode
 # MODEL=64          # for x86 in 64-bit mode
+# MODEL=default     # for others
 MODEL=
 
 # Target ABI
 # ABI=eabi          # for PowerPC / Linux and other SVR4 or EABI platforms
 # ABI=eabi          # for ARM
 # ABI=hardfloat     # for ARM
-# ABI=standard      # for x86
+# ABI=standard      # for others
 ABI=
 
 # Target bit width
-# BITSIZE=64        # for x86 in 64-bit mode
+# BITSIZE=64        # for x86 in 64-bit mode, RiscV in 64-bit mode, AArch64
 # BITSIZE=32        # otherwise
 BITSIZE=
 
 # Target endianness
 # ENDIANNESS=big     # for ARM or PowerPC
-# ENDIANNESS=little  # for ARM or x86
+# ENDIANNESS=little  # for ARM or x86 or RiscV or AArch64
 ENDIANNESS=
 
 # Target operating system and development environment
@@ -728,7 +758,7 @@ ENDIANNESS=
 # SYSTEM=linux
 # SYSTEM=diab
 #
-# Possible choices for ARM:
+# Possible choices for ARM, AArch64, RiscV:
 # SYSTEM=linux
 #
 # Possible choices for x86:
-- 
cgit 


From 50e5009c5a3a2f7515bab08a3e9475e10c5f275d Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Fri, 20 Sep 2019 15:37:02 +0200
Subject: Adding SIMU=k1-cluster -- in configure

---
 configure | 1 +
 1 file changed, 1 insertion(+)

(limited to 'configure')

diff --git a/configure b/configure
index 3bdb5d2b..626bf3aa 100755
--- a/configure
+++ b/configure
@@ -818,6 +818,7 @@ cat >> Makefile.config <<EOF
 ARCHDIRS=$arch $arch/lib $arch/abstractbb $arch/abstractbb/Impure
 EXECUTE=k1-cluster --syscall=libstd_scalls.so --
 CFLAGS= -D __K1C_COS__
+SIMU=k1-cluster -- 
 BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
     Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\
     ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
-- 
cgit