From 4ef8259d18add24bb589a185d050f4a524385f1f Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sun, 27 Jan 2019 16:09:47 +0100
Subject: picosat induces bug in register allocation

---
 test/monniaux/picosat-965/configure.sh | 150 +++++++++++++++++++++++++++++++++
 1 file changed, 150 insertions(+)
 create mode 100755 test/monniaux/picosat-965/configure.sh

(limited to 'test/monniaux/picosat-965/configure.sh')

diff --git a/test/monniaux/picosat-965/configure.sh b/test/monniaux/picosat-965/configure.sh
new file mode 100755
index 00000000..a82cfe87
--- /dev/null
+++ b/test/monniaux/picosat-965/configure.sh
@@ -0,0 +1,150 @@
+#!/bin/sh
+
+satcompetition=no
+
+log=no
+debug=no
+stats=undefined
+trace=undefined
+static=yes
+shared=no
+thirtytwobit=no
+static=no
+rcode=no
+
+while [ $# -gt 0 ]
+do
+  case $1 in
+    -g|--debug) debug=yes;;
+    -O|--optimize) debug=no;;
+    -l|--log) log=yes;;
+    -s|--stats) stats=yes;;
+    -t|--trace) trace=yes;;
+    --no-stats) stats=no;;
+    --no-trace) trace=no;;
+    --no-rcode) rcode=no;;
+    --rcode) rcode=yes;;
+    -32|--32|-m32) thirtytwobit=yes;;
+    -static|--static) static=yes;;
+    -shared|--shared) shared=yes;;
+    *) cat <<EOF
+usage: ./configure.sh [<option> ...]
+
+where <option> is one of the following:
+
+  -g|--debug           include debugging code and symbols
+  -O|--optimize        optimized compilation (default)
+  -l|--log             add low level logging code (default with '-g')
+  -s|--stats           more expensive statististcs (default with '-g')
+  -t|--trace           trace generation (more memory, default with '-g')
+  --no-stats           disable expensive stats
+  --no-trace           enable trace generation
+  -32|--32|-m32        compile for 32 bit machine even on 64 bit host
+  -rcode|--no-rcode    enable/disable compatibility for used in R exension
+  -static|--static     produce static binary
+  -shared|--shared     produce shared library
+EOF
+exit 1
+;;
+  esac
+shift
+done
+
+echo "version ... `cat VERSION`"
+
+if [ $satcompetition = yes ]
+then
+  debug=no
+  stats=no
+  trace=no
+  thirtytwobit=yes
+  static=yes
+  shared=no
+fi
+
+echo "debug ... $debug"
+echo "log ... $log"
+
+[ $stats = undefined ] && stats=$debug
+echo "stats ... $stats"
+
+[ $trace = undefined ] && trace=$debug
+echo "trace ... $trace"
+
+echo "static ... $static"
+
+echo "shared ... $shared"
+
+[ "X$CC" = X ] && CC=gcc
+
+if [ X"$CFLAGS" = X ]
+then
+  case X"$CC" in
+    *wine*|*mingw*) CFLAGS="-DNGETRUSAGE -DNALLSIGNALS";;
+    *);;
+  esac
+  [ $log = yes ] && CFLAGS="$CFLAGS -DLOGGING"
+  [ $stats = yes ] && CFLAGS="$CFLAGS -DSTATS"
+  [ $trace = yes ] && CFLAGS="$CFLAGS -DTRACE"
+  [ $static = yes ] && CFLAGS="$CFLAGS -static"
+  [ $rcode = yes ] && CFLAGS="$CFLAGS -DRCODE"
+  case X"$CC" in
+    X*gcc*)
+      CFLAGS="$CFLAGS -Wall -Wextra"
+      [ $thirtytwobit = yes ] && CFLAGS="$CFLAGS -m32"
+      if [ $debug = yes ]
+      then
+        CFLAGS="$CFLAGS -g3 -ggdb"
+      else
+	CFLAGS="$CFLAGS -DNDEBUG -O3"
+      fi
+      ;;
+    *)
+      if [ $debug = yes ]
+      then
+        CFLAGS="$CFLAGS -g"
+      else
+        CFLAGS="$CFLAGS -O"
+      fi
+      ;;
+  esac
+fi
+
+if [ $rcode = yes ]
+then
+  for rdoth in /usr/share/R/include/R.h $RINC undefined
+  do
+    [ -f $rdoth ] && break
+  done
+  if [ $rdoth = undefined ]
+  then
+    echo "R.h ... not found (add '-I' manually or 'RHEADER=...  ./configure')"
+  else
+    RINC="-I`dirname $rdoth`"
+    CFLAGS="$CFLAGS $RINC"
+    echo "R.h ... added '$RINC' include directive"
+  fi
+  TARGETS="libpicosat.a"
+else
+  TARGETS="picosat picomcs picomus picogcnf libpicosat.a"
+fi
+
+if [ $shared = yes ]
+then
+  TARGETS="$TARGETS libpicosat.so"
+  CFLAGS="$CFLAGS -fPIC"
+fi
+echo "targets ... $TARGETS"
+
+echo "cc ... $CC"
+
+echo "cflags ... $CFLAGS"
+
+printf "makefile ..."
+rm -f makefile
+sed \
+  -e "s,@CC@,$CC," \
+  -e "s,@CFLAGS@,$CFLAGS," \
+  -e "s,@TARGETS@,$TARGETS," \
+makefile.in > makefile
+echo " done"
-- 
cgit