Project

General

Profile

« Previous | Next » 

Revision 3e209698

Added by Pierre-Loïc Garoche almost 9 years ago

First fully working version of horn backend.

Has to be called with "-horn -node main_node"

The test script compute the smt2 file and calls z3 on them.

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