From c974324dadd273d8f62792f400f5db6174c52baf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lukas=20Gr=C3=A4tz?= Date: Fri, 30 Aug 2024 17:03:02 +0200 Subject: [PATCH] add documentation of default for --max-nondet-array-length, see #8428 --- doc/cprover-manual/unsound_options.md | 3 +++ jbmc/src/java_bytecode/java_bytecode_language.h | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/doc/cprover-manual/unsound_options.md b/doc/cprover-manual/unsound_options.md index ebb3d290644..831f72456e8 100644 --- a/doc/cprover-manual/unsound_options.md +++ b/doc/cprover-manual/unsound_options.md @@ -36,6 +36,9 @@ The following options will produce a warning when used with CBMC or JBMC: See [Understanding Loop Unwinding](../cbmc/unwinding/) for an elaboration of these options. +For arrays with unknown length (e.g. input arrays), JBMC has a default limit that +can be changed with the option `--max-nondet-array-length`. + ### Experimental Options Be advised that the following command line options to `cbmc` and `goto-instrument` diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 8eefa379e75..1142e1fee0c 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -63,7 +63,7 @@ Author: Daniel Kroening, kroening@kroening.com "transform `throw` instructions into `assert FALSE` followed by " \ "`assume FALSE`.\n" \ " {y--max-nondet-array-length} {uN} \t " \ - "limit nondet (e.g. input) array size to <= {uN}\n" \ + "limit nondet (e.g. input) array size to <= {uN} (default 5)\n" \ " {y--max-nondet-tree-depth} {uN} \t " \ "limit size of nondet (e.g. input) object tree; at level {uN} references " \ "are set to null\n" \