Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / test-compile.sh @ c02d255e

History | View | Annotate | Download (1.37 KB)

1
#!/bin/bash
2

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

    
9
while IFS=, read -r file main opts
10
do
11
  echo fichier:$file
12
#   echo main:$main
13
 #  echo opts:$opts
14
   rm -f witness*
15
    if [ "$main" != "" ]; then
16
	$LUSTREC -d build -verbose 0 $opts -inline -witnesses -node $main ../$file;
17
    else
18
	$LUSTREC -d build -verbose 0 $opts ../$file
19
    fi
20
    if [ $? -ne 0 ]; then 
21
      rlustrec="INVALID"; 
22
    else 
23
      rlustrec="VALID" 
24
    fi
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";
37
    else
38
      rz3="INVALID"
39
      exit 1
40
    fi    
41
    echo "lustrec ($rlustrec),inlining valid ($rz3),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"
42
# awk 'BEGIN { FS = "\" " } ; { printf "%-20s %-40s\n", $1, $2, $3}' 
43
done < ../tests_ok.nolarge.list