Skip to content

Commit 3b80a4c

Browse files
authored
Add script to text-extract all contracts (#323)
This is a helper script to collect all existing contracts for subsequent review or analysis. This facilitates metrics we want to report. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent e33c59d commit 3b80a4c

File tree

1 file changed

+42
-0
lines changed

1 file changed

+42
-0
lines changed

scripts/find-contracts.sh

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
#!/bin/bash
2+
3+
# Script to find files with specific annotations and print contracts
4+
# containing those annotations up to a line with "fn"
5+
PATTERN_STRING='^\s*#\[((safety::)?(requires|ensures)\(|cfg_attr\((kani|not\(kani\)))'
6+
7+
# Find all files in the git repository that contain any of the patterns
8+
FILES=$(git grep -l -P "$PATTERN_STRING" library/)
9+
10+
if [ -z "$FILES" ]; then
11+
echo "No files found with the specified patterns."
12+
exit 1
13+
fi
14+
15+
# Process each file
16+
for FILE in $FILES; do
17+
echo "=== $FILE ==="
18+
19+
# Use perl to find contracts starting with any pattern and ending at "fn"
20+
cat $FILE | perl -e "
21+
\$in_contract = 0;
22+
\$ws = 0;
23+
while(<>) {
24+
\$line = \$_;
25+
if (!\$in_contract && /$PATTERN_STRING/ && !/^\s*#\[cfg_attr\(kani, derive\(/) {
26+
\$in_contract = 1;
27+
/^(\s*)/;
28+
\$ws = length(\$1);
29+
}
30+
if (\$in_contract) {
31+
\$line =~ s/^ {\$ws}//;
32+
print \$line;
33+
if (\$line =~ /(^| )fn /) {
34+
\$in_contract = 0;
35+
print \"\n\";
36+
}
37+
}
38+
}
39+
"
40+
41+
echo
42+
done

0 commit comments

Comments
 (0)