Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / test-compile.sh @ 7291cb80

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