Project

General

Profile

Download (1.77 KB) Statistics
| Branch: | Tag: | Revision:
1
#!/usr/bin/env bash
2

    
3
bold="\033[1m"
4
red="\033[31m"
5
green="\033[32m"
6
normal="\033[0m"
7

    
8
LUSTREC=$1
9
LUS_FILES=$2
10

    
11
PROVERS=alt-ergo,z3,cvc4
12
TIMEOUT="${TIMEOUT:-30}"
13
JOBS="${JOBS:-16}"
14
FRAMA_C_ARGS="-wp -wp-model ref,real -wp-prover $PROVERS -wp-run-all-provers\
15
    -wp-timeout $TIMEOUT -wp-par $JOBS"
16
FRAMA_C=frama-c
17

    
18
# max length of file names
19
M=0
20
S=0
21
for f in $LUS_FILES
22
do
23
    M=$(( M + 1 ))
24
    if [ "${#f}" -gt "$S" ]; then
25
        S=${#f}
26
    fi
27
done
28

    
29
compile() {
30
    printf "${bold}Compilation tests:${normal}\n"
31
    N=0
32
    OK=0
33
    KO=0
34
    for f in $LUS_FILES
35
    do
36
        N=$(( N + 1 ))
37
        printf "%3.0f%% ${normal}%-${S}s" "$(((100 * N)/M))" "$f"
38
        if $LUSTREC -acsl-spec "$f" >/dev/null 2>/tmp/err; then
39
            OK=$(( OK + 1 ))
40
            CHECK="${green}OK${normal}"
41
        else
42
            KO=$(( KO + 1 ))
43
            ERR=$(</tmp/err)
44
            CHECK="${red}KO\n  $ERR\n${normal}"
45
        fi
46
        printf " %b\n" "${CHECK}"
47
    done
48
    printf "\n${normal}OK: ${green}%d${normal} (${red}%d${normal}) / %d\n\n"\
49
        "${OK}" "${KO}" "${M}"
50
}
51

    
52
verif() {
53
    printf "${bold}Verification tests:${normal}\n"
54
    N=0
55
    OK=0
56
    KO=0
57
    for f in *.c
58
    do
59
        N=$(( N + 1 ))
60
        printf "%3.0f%% ${normal}%-${S}s" "$(((100 * N)/M))" "$f"
61
        if $FRAMA_C $FRAMA_C_ARGS "$f" > /tmp/log; then
62
            sed -n '/Proved goals/{N;N;N;N;p;q}' /tmp/log > "$f".log
63
            OK=$(( OK + 1 ))
64
            LOG=$(<"$f".log)
65
            CHECK="${green}OK\n  $LOG\n${normal}"
66
        else
67
            KO=$(( KO + 1 ))
68
            ERR=$(</tmp/log)
69
            CHECK="${red}KO\n  $ERR\n${normal}"
70
        fi
71
        printf " %b\n" "${CHECK}"
72
    done
73
    printf "\n${normal}OK: ${green}%d${normal} (${red}%d${normal}) / %d\n\n"\
74
        "${OK}" "${KO}" "${M}"
75
}
76

    
77
compile
78

    
79
verif
(1309-1309/1371)