Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / scripts / gen_reports.sh @ 6a93d814

History | View | Annotate | Download (4.26 KB)

1
#!/bin/bash
2

    
3
if [ -e "$1" ]; then
4
    echo "Analyzing $1"
5
else
6
    echo "Input file needed."
7
    exit 2
8
fi
9

    
10
lusfile=$1
11
basename=`basename $1 .lus`
12
build_dir=`dirname $lusfile`/${basename}
13
cfile=${build_dir}/${basename}.c
14
coqfile=${build_dir}/${basename}.coq
15

    
16
script_root=`pwd`/`dirname $0`
17

    
18
reportstyle_root=${script_root}
19
reportstyle_txt="${reportstyle_root}/lustrec_report.report"
20
reportstyle_tex="${reportstyle_root}/lustrec_report_tex.report"
21

    
22
echo ${reportstyle_tex}
23
log=${build_dir}/log
24
rm -f $log
25

    
26
function lustrec_step {
27
echo "***********************************************************************"
28
echo "Generating code: lustrec -d ${build_dir} -acsl-proof $lusfile"
29
echo "***********************************************************************"
30
lustrec -d ${build_dir} -acsl-proof ${lusfile} >& /dev/null
31
b=$?
32
if [ "x$b" == "x0" ]; then
33
    echo "Generated C file" >> $log
34
else
35
    echo "Failed to generate C file" | tee -a $log
36
fi
37
}
38

    
39
function framac_check_step {
40
echo "***********************************************************************"
41
echo "Calling frama-c (type checking) on ${cfile}: frama-c file"
42
echo "***********************************************************************"
43
frama-c $cfile > /dev/null
44
tc=$?
45
if [ "x$tc" == "x0" ]; then
46
    echo "No frama-c typing error" >> $log
47
else
48
    echo "FramaC typing error. See $build_dir/${basename}_report.log" | tee -a $log
49
    frama-c $cfile | grep error | tee $build_dir/${basename}_report.log
50
fi
51
}
52

    
53
function framac_step {
54
echo "***********************************************************************"
55
echo "Calling frama-c on ${cfile}: frama-c -wp ...."
56
echo "***********************************************************************"
57
framaclog=${build_dir}/frama-c.log
58
# Limiting all processes to 2G
59
ulimit -Sv 2000000 
60
timeout 2h \
61
frama-c -wp \
62
-wp-prover CVC4,alt-ergo,z3,coq \
63
$cfile \
64
-wp-par 2 \
65
-wp-model ref \
66
-wp-tactic="Require Why3. unfold itep. hnf. intuition;try why3 \"CVC3\" timelimit 10;try why3 \"Z3\" timelimit 10;why3 \"CVC4\" timelimit 10" \
67
-wp-script $coqfile \
68
-wp-no-let \
69
-wp-report ${reportstyle_txt},${reportstyle_tex} \
70
-wp-report-basename ${build_dir}/$basename 2>&1 | tee ${framaclog}
71
frama=$?
72
if [ "x$frama" == "x0" ]; then
73
    echo "Frama-C ran smoothly." >> $log
74
else
75
    echo "Frama-C error. See ${framaclog}." | tee -a $log
76
fi
77
texreport=${build_dir}/${basename}_report_pdf.tex
78
sed -i "s/_/\\\_/g" ${texreport}
79
# Putting back the limit to usual
80
ulimit -Sv unlimited
81
}
82

    
83
function txt_report_step {
84
# Text report
85
echo "***********************************************************************"
86
echo Generating report
87
echo "***********************************************************************"
88
report_short=${build_dir}/${basename}_report_short.report
89
cat ${build_dir}/${basename}_report.report | grep -v  stmt | grep -v post | grep -v assign > ${report_short} 
90
echo "Results in ${report_short} or ${build_dir}/${basename}_report.report" >> $log
91
}
92

    
93
function tex_report_step {
94
# Latex report
95
echo "***********************************************************************"
96
echo Generating teX report
97
texreport=${build_dir}/${basename}_report_pdf.tex
98
texreport_long=${build_dir}/${basename}_report_pdf_long.tex
99
texreport_short=${build_dir}/${basename}_report_pdf_short.tex
100

    
101

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

    
105
echo "\section{Lustre model: ${basename}}" > ${texreport_short}
106
grep -v "\(stmt\|assign\|post\).*[1-9] \\\\" ${texreport} >> ${texreport_short}
107

    
108
echo Compiling local PDF
109
texreport_local=${build_dir}/${basename}_pdf.tex
110
cat ${script_root}/header_tex.tex ${texreport_short} ${script_root}/footer_tex.tex > ${texreport_local}
111
pdflatex -interaction=nonstopmode -output-directory ${build_dir} ${texreport_local} > /dev/null
112

    
113
echo "PDF version in ${build_dir}/${basename}_pdf.pdf. Source tex in ${build_dir}/${basename}_pdf.tex" >> $log
114
echo "***********************************************************************"
115
}
116

    
117
function clean_step {
118
rm -f *.aux *.log 
119

    
120
}
121

    
122
function print_log {
123
echo ""
124
echo "Main log:"
125
cat $log
126
cat ${report_short}
127
}
128

    
129
lustrec_step
130
[ "x$b" != "x0" ] && print_log && exit 1
131
framac_check_step
132
[ "x$tc" != "x0" ] && print_log && exit 1 
133
framac_step
134
[ "x$frama" != "x0" ] && print_log && exit 1
135
txt_report_step
136
tex_report_step
137
clean_step
138
print_log