Project

General

Profile

Revision e41592cf test/test-compile.sh

View differences:

test/test-compile.sh
131 131
        rgcc2="INVALID";
132 132
    else
133 133
        rgcc2="VALID"
134
    fi	
134
    fi
135 135
    popd > /dev/null
136 136
	# Cheching witness
137 137
    pushd $build > /dev/null
138
    $LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
138
    $LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
139 139
    popd > /dev/null
140 140
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
141 141
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
......
146 146
	rinlining="UNKNOWN";
147 147
    else
148 148
	rinlining="INVALID/TIMEOUT"
149
    fi  
149
    fi
150 150
    if [ $verbose -gt 0 ]; then
151 151
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
152 152
    else
......
166 166
	fi
167 167
	dir=${SRC_PREFIX}/`dirname "$file"`
168 168
	pushd $dir > /dev/null
169
	
169

  
170 170
    # Checking horn backend
171 171
    if [ "$main" != "" ]; then
172 172
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
......
178 178
    else
179 179
        rlustrec="VALID"
180 180
    fi
181
    # echo "z3 $build/$name".smt2 
181
    # echo "z3 $build/$name".smt2
182 182
    # TODO: This part of the script has to be optimized
183 183
    z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null
184 184
    if [ $? -ne 0 ]; then
......
195 195
done < $file_list
196 196
}
197 197

  
198
check_horn () {
199
    while IFS=, read -r file main opts
200
    do
201
	name=`basename "$file" .lus`
202
	if [ "$name" = "$file" ]; then
203
	    return 0
204
	fi
205
	dir=${SRC_PREFIX}/`dirname "$file"`
206
	pushd $dir > /dev/null
207

  
208
    # Checking horn backend
209
    if [ "$main" != "" ]; then
210
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
211
    else
212
	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts "$name".lus
213
    fi
214
    if [ $? -ne 0 ]; then
215
        rlustrec="INVALID";
216
    else
217
        rlustrec="VALID"
218
    fi
219
    if [ $verbose -gt 0 ]; then
220
	echo "lustrec ($rlustrec), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
221
    else
222
	echo "lustrec ($rlustrec), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
223
    fi
224
    popd > /dev/null
225
done < $file_list
226
}
227

  
198 228
usage () {
199 229
echo "usage: $0 [-aciwh] file_list"
200 230
echo "-a: perform all steps"
......
202 232
echo "-i: compile with inline mode"
203 233
echo "-w: compile with inline mode. Check the inlining with z3"
204 234
echo "-h: check files with the horn-pdf backend (requires z3)"
235
echo "-r: regression test for horn backend"
205 236
echo "-v <int>: verbose level"
206 237
}
207 238

  
......
215 246
                -c) nobehavior=0; c=1 ; shift ;;
216 247
                -i) nobehavior=0; i=1 ; shift ;;
217 248
                -w) nobehavior=0; w=1 ; shift ;;
249
                -r) nobehavior=0; r=1 ; shift ;;
218 250
                -h) nobehavior=0; h=1 ; shift ;;
219 251
                --) shift ;;
220 252
                -*) echo "bad option '$1'" ; exit 1 ;;
......
235 267
[ ! -z "$i" ] && inline_compile
236 268
[ ! -z "$w" ] && inline_compile_with_check
237 269
[ ! -z "$h" ] && check_prop
270
[ ! -z "$r" ] && check_horn
238 271
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
239 272

  
240 273

  
......
243 276
	#if [ $? -ne 1 ];then
244 277
	#  rm ../${file}i
245 278
	#fi
246

  

Also available in: Unified diff