From 8d9cdaaceb14732f7030bcba81601ec1d93b9f57 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sun, 26 Jul 2020 10:03:59 +0200
Subject: yet another attempt

---
 test/monniaux/reduced_picosat/reduced_picosat.c |  25 ++++
 test/monniaux/reduced_picosat/testcmp.sh        | 146 ++++++++++++++++++++++++
 2 files changed, 171 insertions(+)
 create mode 100644 test/monniaux/reduced_picosat/reduced_picosat.c
 create mode 100755 test/monniaux/reduced_picosat/testcmp.sh

(limited to 'test/monniaux')

diff --git a/test/monniaux/reduced_picosat/reduced_picosat.c b/test/monniaux/reduced_picosat/reduced_picosat.c
new file mode 100644
index 00000000..e1c18438
--- /dev/null
+++ b/test/monniaux/reduced_picosat/reduced_picosat.c
@@ -0,0 +1,25 @@
+typedef struct b b;
+b *a;
+struct b {
+  int c;
+  int d, **clshead;
+  int **ahead;
+  unsigned h;
+} i;
+b *j();
+int k();
+int main() {
+  a = j();
+  k(a);
+}
+#define e(f) f - g->c
+static void m(b *g, int *l) {
+  if (g)
+    *g->ahead = l;
+}
+b *j() { return &i; }
+int k(b *g) {
+  if (g->d)
+    m(g, e(g->clshead[-1]));
+  return g->h;
+}
diff --git a/test/monniaux/reduced_picosat/testcmp.sh b/test/monniaux/reduced_picosat/testcmp.sh
new file mode 100755
index 00000000..2228c675
--- /dev/null
+++ b/test/monniaux/reduced_picosat/testcmp.sh
@@ -0,0 +1,146 @@
+DEFINES="-DNALARM -DNZIP -DNGETRUSAGE -DNDEBUG"
+COMPCERT=/local/monniaux/Kalray/mppa-RTLpathSE-verif-hash-junk
+DATA=$COMPCERT/test/monniaux/picosat-965/tiny.dat
+CCOMP="$COMPCERT/ccomp -fbitfields -fduplicate 2 -fall-loads-nontrap $DEFINES"
+GCC="kvx-cos-gcc -O -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES"
+HOSTCC0="gcc -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES"
+HOSTCC1="gcc -O -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES"
+HOSTCC2="gcc -O -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror -fsanitize=undefined -fsanitize=address $DEFINES"
+HOSTCC3="gcc -O3 -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES"
+HOSTCC4="clang -Wimplicit -Wuninitialized -Werror $DEFINES"
+HOSTCC5="clang -Wimplicit -Wuninitialized -Werror -fsanitize=undefined -fsanitize=address $DEFINES"
+CFILES="picosat.c"
+SIMU="kvx-cluster --timeout=100000 -- "
+
+if ! $HOSTCC0 $CFILES -o picosat.cc0.host ;
+then exit 30 ;
+fi
+
+if ! $HOSTCC1 $CFILES -o picosat.cc1.host ;
+then exit 31 ;
+fi
+
+if ! $HOSTCC2 $CFILES -o picosat.cc2.host ;
+then exit 32 ;
+fi
+
+if ! $HOSTCC3 $CFILES -o picosat.cc3.host ;
+then exit 33 ;
+fi
+
+if ! $HOSTCC4 $CFILES -o picosat.cc4.host ;
+then exit 34 ;
+fi
+
+if ! $HOSTCC5 $CFILES -o picosat.cc5.host ;
+then exit 35 ;
+fi
+
+timeout 1 ./picosat.cc0.host $DATA 2>&1 > picosat.cc0.out
+if [ $? -ge 100 ];
+then exit 40 ;
+fi
+
+timeout 1 ./picosat.cc1.host $DATA 2>&1 > picosat.cc1.out
+if [ $? -ge 100 ];
+then exit 41 ;
+fi
+
+timeout 1 valgrind --log-file=picosat.cc0.valgrind.log ./picosat.cc0.host $DATA 2>&1 > picosat.cc0.valgrind.out
+if [ $? -ge 100 ];
+then exit 50 ;
+fi
+
+timeout 1 valgrind --log-file=picosat.cc1.valgrind.log ./picosat.cc1.host $DATA 2>&1 > picosat.cc1.valgrind.out
+if [ $? -ge 100 ];
+then exit 51 ;
+fi
+
+timeout 1 ./picosat.cc2.host $DATA 2>&1 > picosat.cc2.out
+if [ $? -ge 100 ];
+then exit 42 ;
+fi
+
+timeout 1 ./picosat.cc3.host $DATA 2>&1 > picosat.cc3.out
+if [ $? -ge 100 ];
+then exit 43 ;
+fi
+
+timeout 1 ./picosat.cc4.host $DATA 2>&1 > picosat.cc4.out
+if [ $? -ge 100 ];
+then exit 44 ;
+fi
+
+timeout 1 ./picosat.cc5.host $DATA 2>&1 > picosat.cc5.out
+if [ $? -ge 100 ];
+then exit 45 ;
+fi
+
+if ! cmp picosat.cc0.out picosat.cc1.out ;
+then exit 60 ;
+fi
+
+if ! cmp picosat.cc0.out picosat.cc0.valgrind.out ;
+then exit 70 ;
+fi
+
+if ! cmp picosat.cc1.out picosat.cc1.valgrind.out ;
+then exit 61 ;
+fi
+
+if ! cmp picosat.cc1.out picosat.cc2.out ;
+then exit 62 ;
+fi
+
+if ! cmp picosat.cc1.out picosat.cc3.out ;
+then exit 63 ;
+fi
+
+if ! $GCC $CFILES -o picosat.gcc.target ;
+then exit 1 ;
+fi
+
+if ! $CCOMP $CFILES -o picosat.ccomp.target ;
+then exit 2 ;
+fi
+
+if ! $CCOMP -fprepass -fprepass= list $CFILES -o picosat.prepass.target ;
+then exit 3 ;
+fi
+
+$SIMU ./picosat.gcc.target $DATA 2>&1 > picosat.gcc.out
+if [ $? -ge 100 ];
+then exit 4 ;
+fi
+
+if ! cmp picosat.gcc.out picosat.cc1.out ;
+then exit 13 ;
+fi
+
+if grep timeout picosat.gcc.out ;
+then exit 8 ;
+fi
+
+$SIMU ./picosat.ccomp.target $DATA 2>&1 > picosat.ccomp.out
+if [ $? -ge 100 ];
+then exit 5 ;
+fi
+
+if grep timeout picosat.ccomp.out ;
+then exit 9 ;
+fi
+
+if ! cmp picosat.gcc.out picosat.ccomp.out ;
+then exit 6 ;
+fi
+
+$SIMU ./picosat.prepass.target $DATA 2>&1 > picosat.prepass.out
+if [ $? -ge 100 ];
+then exit 0 ;
+fi
+
+if cmp picosat.gcc.out picosat.prepass.out ;
+then exit 7 ;
+fi
+
+exit 0
-- 
cgit