Merge branch 'mppa-work' into mppa-abstractbb-dev

1 files changed, 30 insertions, 11 deletions

diff --git a/configure b/configure
index b05fb751..3eb9377b 100755
--- a/configure
+++ b/configure
@@ -55,7 +55,8 @@ Supported targets:
   x86_64-macosx        (x86 64 bits, MacOS X)
   rv32-linux           (RISC-V 32 bits, Linux)
   rv64-linux           (RISC-V 64 bits, Linux)
-  k1c-linux            (Kalray K1c, Linux)
+  k1c-mbr              (Kalray K1c, bare runtime)
+  k1c-cos              (Kalray K1c, ClusterOS)
   manual               (edit configuration file by hand)
 
 For x86 targets, the "x86_32-" prefix can also be written "ia32-" or "i386-".
@@ -440,15 +441,27 @@ if test "$arch" = "mppa_k1c"; then
   #model_options=-m64
   model_options=
   abi="standard"
-  casm="k1-mbr-gcc"
+  if test "$target" = "mbr";
+  then os="mbr";
+  elif test "$target" = "cos";
+  then os="cos";
+  elif test "$target" = "elf";
+  then os="elf";
+  else
+      echo "Unknown K1c backend"
+      exit 1
+  fi
+  osupper=`echo $os|tr a-z A-Z`
+  k1base="k1-$os"
+  casm="$k1base-gcc"
   casm_options="$model_options -c"
-  cc="k1-mbr-gcc $model_options"
-  clinker="k1-mbr-gcc"
+  cc="$k1base-gcc $model_options"
+  clinker="$k1base-gcc"
   bindir="$HOME/.usr/bin"
   libdir="$HOME/.usr/lib"
   clinker_options="$model_options -L$libdir -Wl,-rpath=$libdir"
-  cprepro="k1-mbr-gcc"
-  cprepro_options="$model_options -std=c99 -E -include ccomp_k1c_fixes.h"
+  cprepro="$k1base-gcc"
+  cprepro_options="$model_options -D __K1C_${osupper}__ -std=c99 -E -include ccomp_k1c_fixes.h"
   libmath="-lm"
   system="linux"
 fi
@@ -528,19 +541,19 @@ 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.1|8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0)
+  8.7.0|8.7.1|8.7.2|8.8.0|8.8.1|8.8.2|8.9.0|8.9.1)
         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.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0, 8.6.1"
+            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"
             missingtools=true
         fi;;
   "")
         echo "NOT FOUND"
-        echo "Error: make sure Coq version 8.9.0 is installed."
+        echo "Error: make sure Coq version 8.9.1 is installed."
         missingtools=true;;
 esac
 
@@ -588,7 +601,13 @@ case "$menhir_ver" in
   20[0-9][0-9][0-9][0-9][0-9][0-9])
       if test "$menhir_ver" -ge $MENHIR_REQUIRED -a "$menhir_ver" -le $MENHIR_MAX; then
           echo "version $menhir_ver -- good!"
-          menhir_includes="-I `menhir --suggest-menhirLib`"
+          menhir_include_dir=`menhir --suggest-menhirLib`
+          if test -z "$menhir_include_dir"; then
+              echo "Error: cannot determine the location of the Menhir API library."
+              echo "This can be due to an incorrect Menhir package."
+              echo "Consider using the OPAM package for Menhir."
+              missingtools=true
+          fi
           if test "$menhir_ver" -ge $MENHIR_NEW_API; then
               menhir_flags="--coq-lib-path compcert.cparser.MenhirLib"
           fi
@@ -679,7 +698,7 @@ MANDIR=$sharedir/man
 SHAREDIR=$sharedir
 COQDEVDIR=$coqdevdir
 OCAML_OPT_COMP=$ocaml_opt_comp
-MENHIR_INCLUDES=$menhir_includes
+MENHIR_INCLUDES=-I "$menhir_include_dir"
 MENHIR_FLAGS=$menhir_flags
 COMPFLAGS=-bin-annot
 EOF