Project

General

Profile

Revision 9f77bff7 test/test-compile.sh

View differences:

test/test-compile.sh
5 5
declare c i w h a v
6 6
declare -a files
7 7

  
8
SRC_PREFIX=/Users/Teme/Documents/GitHub/onera_lustrec-tests/
8
SRC_PREFIX=/Users/Teme/Documents/GitHub/lustrec-tests/
9 9
#SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
10 10
NOW=`date "+%y%m%d%H%M"`
11
report=`pwd`/report-1.3-     459-$NOW
11
report=`pwd`/report-1.3-      55-$NOW
12 12
LUSTREC=lustrec
13 13
mkdir -p build
14 14
build=`pwd`"/build"
15 15

  
16 16
gcc_compile() {
17
<<<<<<< HEAD
18
=======
19 17
    if [ $verbose -gt 1 ]; then
20 18
	echo "gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ $1.c > /dev/null"
21 19
    fi
22
>>>>>>> onera_master
23 20
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;
24 21
    if [ $? -ne 0 ]; then
25 22
	rgcc="INVALID";
......
29 26
}
30 27

  
31 28
lustrec_compile() {
32
<<<<<<< HEAD
33
=======
34 29
    if [ $verbose -gt 1 ]; then
35 30
       echo "$LUSTREC $@"
36 31
    fi
37
>>>>>>> onera_master
38 32
    $LUSTREC "$@";
39 33
    if [ $? -ne 0 ]; then
40 34
        rlustrec="INVALID";
......
130 124
	fi
131 125
	dir=${SRC_PREFIX}/`dirname "$file"`
132 126
	pushd $dir > /dev/null
133
<<<<<<< HEAD
134
    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus"
135

  
136
    pushd $build > /dev/null
137
    gcc_compile "$name"
138
	
139
    popd > /dev/null
140
	# Cheching witness
141
    pushd $build > /dev/null
142
    lustrec_compile -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
143
    popd > /dev/null
144
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
145
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
146
	rinlining="VALID";
147
    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
148
	rinlining="ERROR";
149
    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
150
	rinlining="UNKNOWN";
151
    else
152
	rinlining="INVALID/TIMEOUT"
153
    fi  
154
    if [ $verbose -gt 0 ]; then
155
	echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
156
    else
157
	echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
158
    fi
159
    popd > /dev/null
160
=======
161 127

  
162 128
	if [ "$main" != "" ]; then
163 129
	    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;
......
204 170
	else
205 171
	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "TIMEOUT\|INVALID\|ERROR\|UNKNOWN"
206 172
	fi
207
>>>>>>> onera_master
208 173
done < $file_list
209 174

  
210 175
}
......
221 186
	
222 187
    # Checking horn backend
223 188
    if [ "$main" != "" ]; then
224
<<<<<<< HEAD
225
	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
226
    else
227
	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus"
228
=======
229 189
	lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts -node $main $name".lus";
230 190
    else
231 191
	lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts $name".lus"
232
>>>>>>> onera_master
233 192
    fi
234 193

  
235 194
    # echo "z3 $build/$name".smt2 

Also available in: Unified diff