Skip to content

Man pages: improve wording of unwinding-related options #8471

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Sep 25, 2024
Merged

Man pages: improve wording of unwinding-related options #8471

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 12 additions & 9 deletions doc/man/cbmc.1
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -389,13 +389,13 @@ sensitivity size for arrays to 0
\fB\-\-show\-loops\fR
show the loops in the program
.TP
\fB\-\-unwind\fR nr
unwind nr times
\fB\-\-unwind\fR \fInr\fR
unwind all loops at most \fInr\fR times
.TP
\fB\-\-unwindset\fR [T:]L:B,...
unwind loop L with a bound of B
(optionally restricted to thread T)
(use \fB\-\-show\-loops\fR to get the loop IDs)
\fB\-\-unwindset\fR [\fIT\fR:]\fIL\fR:\fIB\fR,...
unwind loop \fIL\fR with a bound of \fIB\fR, optionally restricted to thread
\fIT\fR, and overriding what may be set as default unwinding via
\fB\-\-unwind\fR (use \fB\-\-show\-loops\fR to get the loop IDs)
.TP
\fB\-\-incremental\-loop\fR L
check properties after each unwinding
Expand Down Expand Up @@ -424,11 +424,14 @@ show the verification conditions
remove assignments unrelated to property
.TP
\fB\-\-unwinding\-assertions\fR
generate unwinding assertions (cannot be
used with \fB\-\-cover\fR)
generate unwinding assertions (which are enabled by default; overrides
\fB\-\-no\-unwinding\-assertions\fR when both of these are given); cannot be
used with \fB\-\-cover\fR
.TP
\fB\-\-partial\-loops\fR
permit paths with partial loops
permit paths that execute loops only partially (up to the given unwinding bound)
and then continue beyond the loop even when the loop condition would still hold
(such paths may be spurious, resulting in false alarms)
.TP
\fB\-\-no\-self\-loops\-to\-assumptions\fR
do not simplify while(1){} to assume(0)
Expand Down
8 changes: 5 additions & 3 deletions doc/man/goto-instrument.1
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -849,7 +849,7 @@ empty the function pointer is removed using the standard
show the loops in the program
.TP
\fB\-\-unwind\fR \fInr\fR
unwind nr times
unwind all loops \fInr\fR times
.TP
\fB\-\-unwindset\fR [\fIT\fR:]\fIL\fR:\fIB\fR,...
unwind loop \fIL\fR with a bound of \fIB\fR
Expand All @@ -860,13 +860,15 @@ unwind loop \fIL\fR with a bound of \fIB\fR
read unwindset from file
.TP
\fB\-\-partial\-loops\fR
permit paths with partial loops
permit paths that execute loops only partially (up to the given unwinding bound)
and then continue beyond the loop even when the loop condition would still hold
(such paths may be spurious, resulting in false alarms)
.TP
\fB\-\-no\-unwinding\-assertions\fR
do not generate unwinding assertions
.TP
\fB\-\-unwinding\-assertions\fR
generate unwinding assertions (enabled by default; overrides
generate unwinding assertions (which are enabled by default; overrides
\fB\-\-no\-unwinding\-assertions\fR when both of these are given)
.TP
\fB\-\-continue\-as\-loops\fR
Expand Down
19 changes: 11 additions & 8 deletions doc/man/jbmc.1
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -312,12 +312,12 @@ sensitivity size for arrays to 0
show the loops in the program
.TP
\fB\-\-unwind\fR nr
unwind nr times
unwind all loops at most nr times
.TP
\fB\-\-unwindset\fR [T:]L:B,...
unwind loop L with a bound of B
(optionally restricted to thread T)
(use \fB\-\-show\-loops\fR to get the loop IDs)
\fB\-\-unwindset\fR [\fIT\fR:]\fIL\fR:\fIB\fR,...
unwind loop \fIL\fR with a bound of \fIB\fR, optionally restricted to thread
\fIT\fR, and overriding what may be set as default unwinding via
\fB\-\-unwind\fR (use \fB\-\-show\-loops\fR to get the loop IDs)
.TP
\fB\-\-incremental\-loop\fR L
check properties after each unwinding
Expand Down Expand Up @@ -346,14 +346,17 @@ show the verification conditions
remove assignments unrelated to property
.TP
\fB\-\-unwinding\-assertions\fR
generate unwinding assertions (cannot be
used with \fB\-\-cover\fR)
generate unwinding assertions (which are enabled by default; overrides
\fB\-\-no\-unwinding\-assertions\fR when both of these are given); cannot be
used with \fB\-\-cover\fR
.TP
\fB\-\-no\-unwinding\-assertions\fR
do not generate unwinding assertions
.TP
\fB\-\-partial\-loops\fR
permit paths with partial loops
permit paths that execute loops only partially (up to the given unwinding bound)
and then continue beyond the loop even when the loop condition would still hold
(such paths may be spurious, resulting in false alarms)
.TP
\fB\-\-no\-self\-loops\-to\-assumptions\fR
do not simplify while(1){} to assume(0)
Expand Down
Loading