Project

General

Profile

Revision 1692756a test/test-compile.sh

View differences:

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

  
3
eval set -- $(getopt -n $0 -o "-ciwh:" -- "$@")
3
eval set -- $(getopt -n $0 -o "-aciwvh:" -- "$@")
4 4

  
5
declare c i w h
5
declare c i w h a v
6 6
declare -a files
7 7

  
8
SRC_PREFIX=`svn info | grep Working | sed "s/.*: //"`/lustre_compiler
8 9
NOW=`date "+%y%m%d%H%M"`
9 10
report=`pwd`/report-$NOW
10 11
#LUSTREC="../../_build/src/lustrec"
......
17 18
    while IFS=, read -r file main opts
18 19
    do
19 20
	name=`basename "$file" .lus`
20
	dir=`dirname "$file"`
21
	dir=${SRC_PREFIX}/`dirname "$file"`
21 22
	pushd $dir > /dev/null
22 23
    if [ "$main" != "" ]; then
23 24
	$LUSTREC -d $build -verbose 0 $opts -node $main "$name".lus;
......
51 52
        fi
52 53
    fi
53 54
    popd > /dev/null
54
    echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
55
    if [ $verbose -gt 0 ]; then
56
	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
57
    else
58
	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
59
    fi;
55 60
    done < $file_list
56 61
}
57 62

  
......
59 64
    while IFS=, read -r file main opts
60 65
    do
61 66
	name=`basename "$file" .lus`
62
	dir=`dirname "$file"`
67
	dir=${SRC_PREFIX}/`dirname "$file"`
63 68

  
64 69
	pushd $dir > /dev/null
65 70

  
......
78 83
    else
79 84
        rgcc2="VALID"
80 85
    fi	
81
    echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
86
    if [ $verbose -gt 0 ]; then
87
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
88
    else
89
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
90
    fi;
82 91
    popd > /dev/null
83 92
done < $file_list
84 93
}
......
88 97
    while IFS=, read -r file main opts
89 98
    do
90 99
	name=`basename "$file" .lus`
91
	dir=`dirname "$file"`
100
	dir=${SRC_PREFIX}/`dirname "$file"`
92 101
	pushd $dir > /dev/null
93 102
    $LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
94 103
    if [ $? -ne 0 ]; then
......
119 128
	rinlining="INVALID"
120 129
	exit 1
121 130
    fi  
122
    echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
131
    if [ $verbose -gt 0 ]; then
132
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
133
    else
134
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
135
    fi
123 136
    popd > /dev/null
124 137
done < $file_list
125 138

  
......
129 142
    while IFS=, read -r file main opts
130 143
    do
131 144
	name=`basename "$file" .lus`
132
	dir=`dirname "$file"`
145
	dir=${SRC_PREFIX}/`dirname "$file"`
133 146
	pushd $dir > /dev/null
134 147
	
135 148
    # Checking horn backend
......
146 159
    else
147 160
        rhorn="VALID"
148 161
    fi
149
    echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
162
    if [ $verbose -gt 0 ]; then
163
	echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
164
    else
165
	echo "horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
166
    fi
150 167
    popd > /dev/null
151 168
done < $file_list
152 169
}
......
158 175
echo "-i: compile with inline mode"
159 176
echo "-w: compile with inline mode. Check the inlining with z3"
160 177
echo "-h: check files with the horn-pdf backend (requires z3)"
178
echo "-v <int>: verbose level"
161 179
}
162 180

  
181
verbose=0
163 182
nobehavior=1
164 183

  
165 184
while [ $# -gt 0 ] ; do

Also available in: Unified diff