Skip to content

Commit b32de0a

Browse files
committed
Add classpath option to float to string test and mark it as KNOWNBUG
The test previously passed by accident as it did not specify the models jar via the classpath option of jbmc. Thus, the models were not loaded and the string operations were nondet'ed, and verification failed as required by the test.
1 parent 9089858 commit b32de0a

File tree

1 file changed

+2
-2
lines changed
  • jbmc/regression/jbmc-strings/StringValueOf09

1 file changed

+2
-2
lines changed

jbmc/regression/jbmc-strings/StringValueOf09/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
CORE
1+
KNOWNBUG
22
StringValueOf09.class
3-
--max-nondet-string-length 1000
3+
--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[.*assertion\.1\] .* line 7 .* FAILURE$

0 commit comments

Comments
 (0)