Skip to content

Commit 97a7c25

Browse files
committed
Revert "add documentation of default for --max-nondet-array-length, see #8428"
This reverts commit c974324.
1 parent c974324 commit 97a7c25

File tree

2 files changed

+1
-4
lines changed

2 files changed

+1
-4
lines changed

doc/cprover-manual/unsound_options.md

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -36,9 +36,6 @@ The following options will produce a warning when used with CBMC or JBMC:
3636
See [Understanding Loop Unwinding](../cbmc/unwinding/) for an elaboration of
3737
these options.
3838

39-
For arrays with unknown length (e.g. input arrays), JBMC has a default limit that
40-
can be changed with the option `--max-nondet-array-length`.
41-
4239
### Experimental Options
4340

4441
Be advised that the following command line options to `cbmc` and `goto-instrument`

jbmc/src/java_bytecode/java_bytecode_language.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ Author: Daniel Kroening, [email protected]
6363
"transform `throw` instructions into `assert FALSE` followed by " \
6464
"`assume FALSE`.\n" \
6565
" {y--max-nondet-array-length} {uN} \t " \
66-
"limit nondet (e.g. input) array size to <= {uN} (default 5)\n" \
66+
"limit nondet (e.g. input) array size to <= {uN}\n" \
6767
" {y--max-nondet-tree-depth} {uN} \t " \
6868
"limit size of nondet (e.g. input) object tree; at level {uN} references " \
6969
"are set to null\n" \

0 commit comments

Comments
 (0)