Project

General

Profile

Revision c02d255e test/test-compile.sh

View differences:

test/test-compile.sh
1 1
#!/bin/bash
2 2

  
3 3
NOW=`date "+%y%m%d%H%M"`
4
LUSTREC="../../_build/src/lustrec"
4
#LUSTREC="../../_build/src/lustrec"
5
LUSTREC=lustrec
5 6
mkdir -p build
6 7
cd build
7 8

  
8 9
while IFS=, read -r file main opts
9 10
do
10
#   echo fichier:$file
11
  echo fichier:$file
11 12
#   echo main:$main
12
#   echo opts:$opts
13
 #  echo opts:$opts
14
   rm -f witness*
13 15
    if [ "$main" != "" ]; then
14
	$LUSTREC -d build -verbose 0 $opts -node $main ../$file;
16
	$LUSTREC -d build -verbose 0 $opts -inline -witnesses -node $main ../$file;
15 17
    else
16 18
	$LUSTREC -d build -verbose 0 $opts ../$file
17 19
    fi
......
20 22
    else 
21 23
      rlustrec="VALID" 
22 24
    fi
23
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null
24
    if [ $? -ne 0 ]; then
25
      rgcc="INVALID";
25
  #  echo "horn encoding: lustreh -horn -node check witness.lus 2>/dev/nul"
26
    lustreh -horn -node check witness.lus 2>/dev/null
27
    #    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null
28
   # echo "Calling z3: "
29
    z3="`z3 -t:10 witness.smt2 | xargs`"
30
    #echo "Test: $z3"
31
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
32
      rz3="VALID";
33
    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
34
      rz3="ERROR";
35
    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
36
      rz3="UNKNOWN";
26 37
    else
27
      rgcc="VALID"
38
      rz3="INVALID"
39
      exit 1
28 40
    fi    
29
    echo "lustrec ($rlustrec),gcc ($rgcc),diff with ref ($rdiff),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep INVALID
41
    echo "lustrec ($rlustrec),inlining valid ($rz3),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"
30 42
# awk 'BEGIN { FS = "\" " } ; { printf "%-20s %-40s\n", $1, $2, $3}' 
31
done < ../tests_ok.list
43
done < ../tests_ok.nolarge.list

Also available in: Unified diff