Skip to content

Commit b17a993

Browse files
committed
List supported coverage criteria in CBMC's help output
Rather than making the user read further documentation, list all (currently) supported coverage criteria when running cbmc --help. For consistency, also add "assumes" as an alternative way to request coverage of assume statements (previously only "assume" was supported, even though we otherwise included the plural variants where applicable).
1 parent b345e2a commit b17a993

File tree

2 files changed

+7
-2
lines changed

2 files changed

+7
-2
lines changed

src/goto-instrument/cover.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@ parse_coverage_criterion(const std::string &criterion_string)
130130
c = coverage_criteriont::MCDC;
131131
else if(criterion_string == "cover")
132132
c = coverage_criteriont::COVER;
133-
else if(criterion_string == "assume")
133+
else if(criterion_string == "assume" || criterion_string == "assumes")
134134
c = coverage_criteriont::ASSUME;
135135
else
136136
{

src/goto-instrument/cover.h

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,12 @@ class optionst;
3131

3232
#define HELP_COVER \
3333
" --cover CC create test-suite with coverage criterion " \
34-
"CC\n" \
34+
"CC,\n" \
35+
" where CC is one of assertion[s], " \
36+
"assume[s],\n" \
37+
" branch[es], condition[s], cover, " \
38+
"decision[s],\n" \
39+
" location[s], or mcdc\n" \
3540
" --cover-failed-assertions do not stop coverage checking at failed " \
3641
"assertions\n" \
3742
" (this is the default for --cover " \

0 commit comments

Comments
 (0)