-
Notifications
You must be signed in to change notification settings - Fork 3
/
verifyAllOpt.sh
executable file
·79 lines (72 loc) · 2.92 KB
/
verifyAllOpt.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
#! /bin/bash
RED='\033[0;31m'
GREEN='\033[0;32m'
BLUE='\033[0;34m'
NC='\033[0m' # No Color
error=0
processedfiles=0
basedir="src/dafny/smart"
# verify each folder with a suitable verifier configuration
# src/dafny/smart/algorithms
# dafny3 /dafnyVerify:1 /compile:0 /tracePOs /traceTimes /trace CommuteProof.dfy
# dafny3 /dafnyVerify:1 /compile:0 /tracePOs /traceTimes /trace IndexBasedAlgorithm.dfy
# dafny3 /dafnyVerify:1 /compile:0 /tracePOs /traceTimes /trace MainAlgorithm.dfy
# dafny3 /dafnyVerify:1 /compile:0 /tracePOs /traceTimes /trace OptimalAlgorithm.dfy
for value in algorithms helpers paths seqofbits synthattribute trees .
# for value in "./"
# for value in trees
do
echo -e "${BLUE}-------------------------------------------------------${NC}"
echo -e "${BLUE}==> Processing *.dfy files in subdir $basedir/$value"
echo -e "${BLUE}-------------------------------------------------------${NC}"
for entry in "$basedir/$value"/*.dfy
do
processedfiles=$((processedfiles + 1))
# echo -e "${BLUE}-------------------------------------------------------${NC}"
echo -e "${BLUE}Processing $entry${NC}"
# dafny /dafnyVerify:1 /compile:0 /tracePOs /traceTimes /trace /noCheating:1 $entry
dafny /dafnyVerify:1 /compile:0 /tracePOs /traceTimes /trace /noCheating:1 /proverWarnings:1 /vcsMaxKeepGoingSplits:10 /vcsCores:12 /vcsMaxCost:1000 /vcsKeepGoingTimeout:10 /restartProver /verifySeparately $entry
# echo "$result"
if [ $? -eq 0 ]
then
echo -e "${GREEN}No errors in $entry${NC}"
else
echo -e "${RED}Some errors occured in $entry${NC}"
error=$((error + 1))
fi
done
echo -e "${BLUE}-------------------------------------------------------${NC}"
if [ $error -ne 0 ]
then
echo -e "${RED}Some files [$error/$processedfiles] has(ve) errors :-("
# exit 1
else
echo -e "${GREEN}No errors occured in $processedfiles files! Great job.${NC}"
# exit 0
fi
echo -e "${BLUE}<== [DONE] subdir $basedir/$value"
echo -e "${BLUE}-------------------------------------------------------${NC}"
done
# for entry in "$1"/*.dfy
# do
# processedfiles=$((processedfiles + 1))
# echo -e "${BLUE}-------------------------------------------------------${NC}"
# echo -e "${BLUE}Processing $entry${NC}"
# dafny3 /dafnyVerify:1 /compile:0 /tracePOs /traceTimes /trace /noCheating:1 /proverWarnings:1 /vcsMaxKeepGoingSplits:10 /vcsCores:12 /vcsMaxCost:1000 /vcsKeepGoingTimeout:8 /restartProver /verifySeparately "$entry"
# # echo "$result"
# if [ $? -eq 0 ]
# then
# echo -e "${GREEN}No errors in $entry${NC}"
# else
# echo -e "${RED}Some errors occured in $entry${NC}"
# error=$((error + 1))
# fi
# done
# if [ $error -ne 0 ]
# then
# echo -e "${RED}Some files [$error/$processedfiles] has(ve) errors :-("
# exit 1
# else
# echo -e "${GREEN}No errors occured! Great job.${NC}"
# exit 0
# fi