Project

General

Profile

Revision cd6efd9b test/test-compile.sh

View differences:

test/test-compile.sh
11 11
#   echo main:$main
12 12
#   echo opts:$opts
13 13
    if [ "$main" != "" ]; then
14
	$LUSTREC -d build -verbose 0 $opts -node $main ../$file;
14
	$LUSTREC -horn -d build -verbose 0 $opts -node $main ../$file;
15 15
    else
16
	$LUSTREC -d build -verbose 0 $opts ../$file
16
	$LUSTREC -horn -d build -verbose 0 $opts ../$file 
17 17
    fi
18 18
    if [ $? -ne 0 ]; then 
19 19
      rlustrec="INVALID"; 
20 20
    else 
21 21
      rlustrec="VALID" 
22 22
    fi
23
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null
23
    echo z3 `basename $file .lus`.smt2 | grep unsat 
24
    z3 `basename $file .lus`.smt2 | grep unsat > /dev/null
24 25
    if [ $? -ne 0 ]; then
25
      rgcc="INVALID";
26
      rz3="INVALID";
26 27
    else
27
      rgcc="VALID"
28
      rz3="VALID"
28 29
    fi    
29
    echo "lustrec ($rlustrec),gcc ($rgcc),diff with ref ($rdiff),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep INVALID
30
    echo "lustrec -horn ($rlustrec),z3 ($rz3),diff with ref ($rdiff),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep INVALID
30 31
# awk 'BEGIN { FS = "\" " } ; { printf "%-20s %-40s\n", $1, $2, $3}' 
31 32
done < ../tests_ok.list

Also available in: Unified diff