Project

General

Profile

« Previous | Next » 

Revision c02d255e

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

Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test script modified to check consistency of the inlining process

View differences:

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

  		




  3
  3
  
    
NOW=`date "+%y%m%d%H%M"`


  		




  4
  
  
    
LUSTREC="../../_build/src/lustrec"


  		




  
  4
  
    
#LUSTREC="../../_build/src/lustrec"


  		




  
  5
  
    
LUSTREC=lustrec


  		




  5
  6
  
    
mkdir -p build


  		




  6
  7
  
    
cd build


  		




  7
  8
  
    

  		




  8
  9
  
    
while IFS=, read -r file main opts


  		




  9
  10
  
    
do


  		




  10
  
  
    
#   echo fichier:$file


  		




  
  11
  
    
  echo fichier:$file


  		




  11
  12
  
    
#   echo main:$main


  		




  12
  
  
    
#   echo opts:$opts


  		




  
  13
  
    
 #  echo opts:$opts


  		




  
  14
  
    
   rm -f witness*


  		




  13
  15
  
    
    if [ "$main" != "" ]; then


  		




  14
  
  
    
	$LUSTREC -d build -verbose 0 $opts -node $main ../$file;


  		




  
  16
  
    
	$LUSTREC -d build -verbose 0 $opts -inline -witnesses -node $main ../$file;


  		




  15
  17
  
    
    else


  		




  16
  18
  
    
	$LUSTREC -d build -verbose 0 $opts ../$file


  		




  17
  19
  
    
    fi


  		




  ......




  20
  22
  
    
    else 


  		




  21
  23
  
    
      rlustrec="VALID" 


  		




  22
  24
  
    
    fi


  		




  23
  
  
    
    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null


  		




  24
  
  
    
    if [ $? -ne 0 ]; then


  		




  25
  
  
    
      rgcc="INVALID";


  		




  
  25
  
    
  #  echo "horn encoding: lustreh -horn -node check witness.lus 2>/dev/nul"


  		




  
  26
  
    
    lustreh -horn -node check witness.lus 2>/dev/null


  		




  
  27
  
    
    #    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null


  		




  
  28
  
    
   # echo "Calling z3: "


  		




  
  29
  
    
    z3="`z3 -t:10 witness.smt2 | xargs`"


  		




  
  30
  
    
    #echo "Test: $z3"


  		




  
  31
  
    
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then


  		




  
  32
  
    
      rz3="VALID";


  		




  
  33
  
    
    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then


  		




  
  34
  
    
      rz3="ERROR";


  		




  
  35
  
    
    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then


  		




  
  36
  
    
      rz3="UNKNOWN";


  		




  26
  37
  
    
    else


  		




  27
  
  
    
      rgcc="VALID"


  		




  
  38
  
    
      rz3="INVALID"


  		




  
  39
  
    
      exit 1


  		




  28
  40
  
    
    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


  		




  
  41
  
    
    echo "lustrec ($rlustrec),inlining valid ($rz3),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"


  		




  30
  42
  
    
# awk 'BEGIN { FS = "\" " } ; { printf "%-20s %-40s\n", $1, $2, $3}' 


  		




  31
  
  
    
done < ../tests_ok.list


  		




  
  43
  
    
done < ../tests_ok.nolarge.list


  		












Also available in:  Unified diff