Project

General

Profile

Revision 8b3afe43 test/test-compile.sh

View differences:

test/test-compile.sh
4 4
#LUSTREC="../../_build/src/lustrec"
5 5
LUSTREC=lustrec
6 6
mkdir -p build
7
cd build
8

  
7
build=`pwd`"/build"
9 8
while IFS=, read -r file main opts
10 9
do
11 10
  echo fichier:$file
12 11
#   echo main:$main
13
 #  echo opts:$opts
12
#   echo opts:$opts
14 13
    rm -f witness*
14
    name=`basename "$file" .lus`
15
    dir=`dirname "$file"`
16
    pushd $dir > /dev/null
15 17
    if [ "$main" != "" ]; then
16
        $LUSTREC -d build -verbose 0 $opts -node $main ../$file;
18
	$LUSTREC -d $build -verbose 0 $opts -node $main "$name".lus;
17 19
        if [ $? -ne 0 ]; then
18 20
          rlustrec1="INVALID";
19 21
        else
20 22
          rlustrec1="VALID"
21 23
	fi
22
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null
24
	pushd $build > /dev/null
25
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
26
	popd > /dev/null
23 27
        if [ $? -ne 0 ]; then
24 28
          rgcc1="INVALID";
25 29
        else
26 30
          rgcc1="VALID"
27 31
	fi	
28 32
	# Removing Generated lusi file
29
	grep generated ../${file}i > /dev/null
30
	if [ $? -ne 1 ];then
31
	  rm ../${file}i
32
	fi
33
	#grep generated ../${file}i > /dev/null
34
	#if [ $? -ne 1 ];then
35
	#  rm ../${file}i
36
	#fi
33 37
	# Checking inlining
34
	$LUSTREC -d build -verbose 0 $opts -inline -witnesses -node $main ../$file;
38
	$LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
35 39
	if [ $? -ne 0 ]; then
36 40
          rlustrec2="INVALID";
37 41
        else
38 42
          rlustrec2="VALID"
39 43
	fi
40
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null
44
	pushd $build > /dev/null
45
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
46
	popd > /dev/null
41 47
        if [ $? -ne 0 ]; then
42 48
          rgcc2="INVALID";
43 49
        else
44 50
          rgcc2="VALID"
45 51
	fi	
46 52
	# Cheching witness
53
	pushd $build > /dev/null
47 54
	lustreh -horn -node check witness.lus 2>/dev/null
55
	popd > /dev/null
48 56
    	z3="`z3 -t:10 witness.smt2 | xargs`"
49 57
    	if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
50 58
	  rinlining="VALID";
......
57 65
	 exit 1
58 66
        fi  
59 67
	# Checking horn backend
60
	$LUSTREC -horn -d build -verbose 0 $opts -node $main ../$file;
61
	echo z3 `basename $file .lus`.smt2 | grep unsat
68
	$LUSTREC -horn -d $build -verbose 0 $opts -node $main "$name".lus;
69
	echo z3 "$name".smt2 | grep unsat
62 70
	# TODO: This part of the script has to be optimized
63
	z3 -t:10 `basename $file .lus`.smt2 | grep unsat > /dev/null
71
	z3 -t:10 "$name".smt2 | grep unsat > /dev/null
64 72
	if [ $? -ne 0 ]; then
65 73
         rhorn="INVALID";
66 74
        else
......
68 76
        fi
69 77
	echo "lustrec ($rlustrec1),gcc($rgcc1),lustrec inline ($rlustrec2), gcc inline ($rgcc2), inlining valid ($rinlining),horn ($rhorn),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"
70 78
    else
71
	$LUSTREC -d build -verbose 0 $opts ../$file;
79
	$LUSTREC -d $build -verbose 0 $opts "$name".lus;
72 80
        if [ $? -ne 0 ]; then
73 81
          rlustrec1="INVALID";
74 82
        else
75 83
          rlustrec1="VALID"
76 84
        fi
77
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null
85
	pushd $build > /dev/null
86
        gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
87
	popd > /dev/null
78 88
        if [ $? -ne 0 ]; then
79 89
          rgcc1="INVALID";
80 90
        else
81 91
          rgcc1="VALID"
82 92
        fi
83
	$LUSTREC -horn -d build -verbose 0 $opts ../$file 
93
	$LUSTREC -horn -d $build -verbose 0 $opts ../$file 
84 94
	echo "lustrec ($rlustrec1), gcc($rgcc1), horn($rhorn), `dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"
85 95
    fi
86
done < ../tests_ok.list
96
    popd > /dev/null
97
done < tests_ok.list

Also available in: Unified diff