Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / test-compile.sh @ cd6efd9b

History | View | Annotate | Download (919 Bytes)

1
#!/bin/bash
2

    
3
NOW=`date "+%y%m%d%H%M"`
4
LUSTREC="../../_build/src/lustrec"
5
mkdir -p build
6
cd build
7

    
8
while IFS=, read -r file main opts
9
do
10
#   echo fichier:$file
11
#   echo main:$main
12
#   echo opts:$opts
13
    if [ "$main" != "" ]; then
14
	$LUSTREC -horn -d build -verbose 0 $opts -node $main ../$file;
15
    else
16
	$LUSTREC -horn -d build -verbose 0 $opts ../$file 
17
    fi
18
    if [ $? -ne 0 ]; then 
19
      rlustrec="INVALID"; 
20
    else 
21
      rlustrec="VALID" 
22
    fi
23
    echo z3 `basename $file .lus`.smt2 | grep unsat 
24
    z3 `basename $file .lus`.smt2 | grep unsat > /dev/null
25
    if [ $? -ne 0 ]; then
26
      rz3="INVALID";
27
    else
28
      rz3="VALID"
29
    fi    
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
31
# awk 'BEGIN { FS = "\" " } ; { printf "%-20s %-40s\n", $1, $2, $3}' 
32
done < ../tests_ok.list