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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
#!/usr/bin/env bash
set -e
CXX=$1
shift
# if a command-line argument is provided, use it as a path to built binaries
# (CMake-style build); otherwise assume we use Makefile-based in-tree build
if [ $# -eq 1 ] ; then
bin_dir=$(cd $1 ; pwd)
else
unset bin_dir
fi
echo $bin_dir
# make sure we execute the remainder in the directory containing this script
cd `dirname $0`
missing_options=0
# we don't check goto-cc for now
# we omit crangler for it doesn't take options other than help or a file name
for t in \
../jbmc/src/janalyzer \
../jbmc/src/jbmc \
../jbmc/src/jdiff \
../src/cbmc \
../src/goto-analyzer \
../src/goto-diff \
../src/goto-harness \
../src/goto-instrument \
../src/memory-analyzer \
../src/symtab2gb \
; do
tool_name=$(basename $t)
opt_name=$(echo $tool_name | tr 'a-z-' 'A-Z_')
echo "Extracting the raw list of parameters from $tool_name"
$CXX -E -dM -std=c++17 -I../src -I../jbmc/src $t/*_parse_options.cpp -o macros.c
# goto-analyzer partly uses the spelling "analyser" within the code base
echo ${opt_name}_OPTIONS | sed 's/GOTO_ANALYZER/GOTO_ANALYSER/' >> macros.c
rawstring="`$CXX -E -P -w macros.c` \"?h(help)\""
rm macros.c
# now the main bit, convert from raw format to a proper list of switches
cleanstring=`(
# extract 2-hyphen switches, such as --foo
# grep for '(foo)' expressions, and then use sed to remove parantheses and
# put '-' at the start (we accept both --X and -X)
(echo $rawstring | grep -o "([^)]*)" | sed "s/^.\(.*\).$/-\1/") ;
# extract 1-hyphen switches, such as -F
# use sed to remove all (foo) expressions, then you're left with switches
# and ':', so grep the colons out and then use sed to include the '-'
(echo $rawstring | sed "s/([^)]*)//g" | grep -o "[a-zA-Z0-9?]" | sed "s/\(.*\)/-\1/")
) | sed 's/" "//g'`
if [ "x$bin_dir" = "x" ] ; then
tool_bin=$t/$tool_name
else
tool_bin=$bin_dir/$tool_name
fi
if [ ! -x $tool_bin ] ; then
echo "$tool_bin is not an executable, cannot check help completeness"
continue
fi
$tool_bin --help > help_string
grep '^\\fB\\-' ../doc/man/$tool_name.1 > man_page_opts
# some options are intentionally undocumented
case $tool_name in
cbmc)
for undoc in \
-all-claims -all-properties -claim -show-claims \
-document-subgoals \
-no-propagation -no-simplify -no-simplify-if \
-floatbv -no-unwinding-assertions \
-slice-by-trace ; do
echo "$undoc" >> help_string
echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts
done
;;
goto-analyzer)
for undoc in -show-intervals -show-non-null ; do
echo "$undoc" >> help_string
echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts
done
;;
# We also need ignore the negative default checks for goto-instrument given
# that it's not processing them (but still ends up importing them by using
# the macro PARSE_OPTIONS_GOTO_CHECK). The rationale for ignoring them is
# similar to the goto-diff entry below.
goto-instrument)
for undoc in \
-document-claims-html -document-claims-latex -show-claims \
-no-simplify -no-pointer-check -no-bounds-check -no-undefined-shift-check \
-no-pointer-primitive-check -no-div-by-zero-check -no-signed-overflow-check ; do
echo "$undoc" >> help_string
echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts
done
;;
# goto-diff is a bit of a peculiar situation in that it initialises some
# of its options using the PARSE_OPTIONS_GOTO_CHECK macro which initialises
# the negative checks (being the mirror image of the default checks), which
# this tool doesn't make use of - but there's also no good way to remove
# given our current architecture. Thus, we just don't document them (and
# ignore them if someone falls on them by accident).
goto-diff)
for undoc in \
-no-pointer-check -no-bounds-check -no-undefined-shift-check \
-no-pointer-primitive-check -no-div-by-zero-check \
-no-signed-overflow-check ; do
echo "$undoc" >> help_string
echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts
done
;;
janalyzer)
# -jar, -gb are documented, but in a different format
for undoc in -show-intervals -show-non-null -jar -gb ; do
echo "$undoc" >> help_string
echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts
done
;;
jbmc)
# -jar, -gb are documented, but in a different format
for undoc in \
-document-subgoals \
-no-propagation -no-simplify -no-simplify-if \
-no-unwinding-assertions \
-jar -gb ; do
echo "$undoc" >> help_string
echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts
done
;;
esac
for opt in $cleanstring ; do
if ! grep -q -- $opt help_string ; then
echo "Option $opt of $tool_name is undocumented"
missing_options=1
fi
case $opt in
-help|-h|-?) continue ;;
-version) continue ;;
esac
m_opt=$(echo $opt | sed 's/-/\\\\-/g')
if ! grep -q -- "$m_opt" man_page_opts ; then
echo "Option $opt of $tool_name is missing from its man page"
missing_options=1
fi
done
rm help_string
rm man_page_opts
done
if [ $missing_options -eq 1 ] ; then
echo "Undocumented options found"
exit 1
else
echo "All options are documented"
exit 0
fi
|
