CristalCaveGem » LustreC

#!/bin/bash

if [ -e "$1" ]; then

    echo "Analyzing $1"

else

    echo "Input file needed."

    exit 2

fi

lusfile=$1

basename=`basename $1 .lus`

build_dir=`dirname $lusfile`/${basename}

cfile=${build_dir}/${basename}.c

coqfile=${build_dir}/${basename}.coq

script_root=`pwd`/`dirname $0`

reportstyle_root=${script_root}

reportstyle_txt="${reportstyle_root}/lustrec_report.report"

reportstyle_tex="${reportstyle_root}/lustrec_report_tex.report"

echo ${reportstyle_tex}

log=${build_dir}/log

rm -f $log

function lustrec_step {

echo "***********************************************************************"

echo "Generating code: lustrec -d ${build_dir} -acsl-proof $lusfile"

echo "***********************************************************************"

lustrec -d ${build_dir} -acsl-proof ${lusfile} >& /dev/null

b=$?

if [ "x$b" == "x0" ]; then

    echo "Generated C file" >> $log

else

    echo "Failed to generate C file" | tee -a $log

fi

}

function framac_check_step {

echo "***********************************************************************"

echo "Calling frama-c (type checking) on ${cfile}: frama-c file"

echo "***********************************************************************"

frama-c $cfile > /dev/null

tc=$?

if [ "x$tc" == "x0" ]; then

    echo "No frama-c typing error" >> $log

else

    echo "FramaC typing error. See $build_dir/${basename}_report.log" | tee -a $log

    frama-c $cfile | grep error | tee $build_dir/${basename}_report.log

fi

}

function framac_step {

echo "***********************************************************************"

echo "Calling frama-c on ${cfile}: frama-c -wp ...."

echo "***********************************************************************"

framaclog=${build_dir}/frama-c.log

# Limiting all processes to 2G

ulimit -Sv 2000000 

timeout 2h \

frama-c -wp \

-wp-prover CVC4,alt-ergo,z3,coq \

$cfile \

-wp-par 2 \

-wp-model ref \

-wp-tactic="Require Why3. unfold itep. hnf. intuition;try why3 \"CVC3\" timelimit 10;try why3 \"Z3\" timelimit 10;why3 \"CVC4\" timelimit 10" \

-wp-script $coqfile \

-wp-no-let \

-wp-report ${reportstyle_txt},${reportstyle_tex} \

-wp-report-basename ${build_dir}/$basename 2>&1 | tee ${framaclog}

frama=$?

if [ "x$frama" == "x0" ]; then

    echo "Frama-C ran smoothly." >> $log

else

    echo "Frama-C error. See ${framaclog}." | tee -a $log

fi

texreport=${build_dir}/${basename}_report_pdf.tex

sed -i "s/_/\\\_/g" ${texreport}

# Putting back the limit to usual

ulimit -Sv unlimited

}

function txt_report_step {

# Text report

echo "***********************************************************************"

echo Generating report

echo "***********************************************************************"

report_short=${build_dir}/${basename}_report_short.report

cat ${build_dir}/${basename}_report.report | grep -v  stmt | grep -v post | grep -v assign > ${report_short} 

echo "Results in ${report_short} or ${build_dir}/${basename}_report.report" >> $log

}

function tex_report_step {

# Latex report

echo "***********************************************************************"

echo Generating teX report

texreport=${build_dir}/${basename}_report_pdf.tex

texreport_long=${build_dir}/${basename}_report_pdf_long.tex

texreport_short=${build_dir}/${basename}_report_pdf_short.tex

echo "\section{Lustre model: `echo ${basename} | sed \"s/_/-/g\"`}" > ${texreport_long}

cat ${texreport} >> ${texreport_long}

echo "\section{Lustre model: ${basename}}" > ${texreport_short}

grep -v "\(stmt\|assign\|post\).*[1-9] \\\\" ${texreport} >> ${texreport_short}

echo Compiling local PDF

texreport_local=${build_dir}/${basename}_pdf.tex

cat ${script_root}/header_tex.tex ${texreport_short} ${script_root}/footer_tex.tex > ${texreport_local}

pdflatex -interaction=nonstopmode -output-directory ${build_dir} ${texreport_local} > /dev/null

echo "PDF version in ${build_dir}/${basename}_pdf.pdf. Source tex in ${build_dir}/${basename}_pdf.tex" >> $log

echo "***********************************************************************"

}

function clean_step {

rm -f *.aux *.log 

}

function print_log {

echo ""

echo "Main log:"

cat $log

cat ${report_short}

}

lustrec_step

[ "x$b" != "x0" ] && print_log && exit 1

framac_check_step

[ "x$tc" != "x0" ] && print_log && exit 1 

framac_step

[ "x$frama" != "x0" ] && print_log && exit 1

txt_report_step

tex_report_step

clean_step

print_log