Skip to content

Commit cf0572e

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #4768 from peterschrammel/add-string-format-verification-tests
Upstream string format verification tests
2 parents 86499a6 + f65b0db commit cf0572e

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

57 files changed

+767
-1
lines changed

‎jbmc/lib/java-models-library

Submodule java-models-library updated 30 files

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_alternative.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_alternative --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
TG-2897

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_alternative_uppercase.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_alternative_uppercase --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
TG-2897

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_boolean.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_boolean --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_boolean_null.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_boolean_null --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
TG-2899

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_boolean_upper.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_boolean_upper --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_braces.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
FUTURE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_braces --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
Flags in format specifiers are not supported yet.

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_character.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_character --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_character_uppercase.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_character_uppercase --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_exponent.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_exponent --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
TG-2897

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_exponent_float_arg.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_exponent_float_arg --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
TG-2532

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_exponent_uppercase.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_exponent_uppercase --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
TG-2897

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_float.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_float --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
--
9+
TG-2897

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_general_scientific.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_general_scientific --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
TG-2897

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_general_scientific_uppercase.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_general_scientific_uppercase --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
TG-2897

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_hash.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
FUTURE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_hash --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
Hash codes are not supported yet.

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_hex.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_hex --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_hex_upper.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
FUTURE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_hex_upper --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
This fails due to a missing case in the string solver.

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_integer.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_integer --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_leading_spaces.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
FUTURE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_leading_spaces --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
Flags and width in format specifiers are not supported yet.

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_leading_zeros.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
FUTURE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_leading_zeros --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
Flags and width in format specifiers are not supported yet.

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_locale.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_locale --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_new_line.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_new_line --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
String.format does not work when the argument list is empty (which is a valid thing
11+
to do if all format specifiers are of type %% or %n).

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_octal.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
FUTURE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_octal --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
This type of format specifier is not supported yet.

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_percent.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
FUTURE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_percent --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
This test passes but doesn't actually reach the assertion due to conflicting lemmas in the string solver.
11+
The problem is that String.format does not work when the argument list is empty (which is a valid thing
12+
to do if all format specifiers are of type %% or %n).

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_plus_sign.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
FUTURE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_plus_sign --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
Flags in format specifiers are not supported yet.

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_plus_sign_negative.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
FUTURE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_plus_sign_negative_value --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
Flags in format specifiers are not supported yet.

‎jbmc/regression/jbmc-strings/StringFormatVerification/check_separators.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
FUTURE
2+
test.class
3+
--max-nondet-string-length 20 --function test.check_separators --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^ignoring
9+
--
10+
Flags in format specifiers are not supported yet.

‎jbmc/regression/jbmc-strings/StringFormatVerification/fail_alternative.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.fail_alternative --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
TG-2897

‎jbmc/regression/jbmc-strings/StringFormatVerification/fail_alternative_uppercase.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.fail_alternative_uppercase --verbosity 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
TG-2897

‎jbmc/regression/jbmc-strings/StringFormatVerification/fail_boolean.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
test.class
3+
--max-nondet-string-length 20 --function test.fail_boolean --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--

‎jbmc/regression/jbmc-strings/StringFormatVerification/fail_boolean_null.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.fail_boolean_null --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
TG-2899

‎jbmc/regression/jbmc-strings/StringFormatVerification/fail_boolean_upper.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
test.class
3+
--max-nondet-string-length 20 --function test.fail_boolean_upper --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--

‎jbmc/regression/jbmc-strings/StringFormatVerification/fail_braces.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
FUTURE
2+
test.class
3+
--max-nondet-string-length 20 --function test.fail_braces --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
Flags in format specifiers are not supported yet.

‎jbmc/regression/jbmc-strings/StringFormatVerification/fail_character.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
test.class
3+
--max-nondet-string-length 20 --function test.fail_character --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--

‎jbmc/regression/jbmc-strings/StringFormatVerification/fail_character_uppercase.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
test.class
3+
--max-nondet-string-length 20 --function test.fail_character_uppercase --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--

‎jbmc/regression/jbmc-strings/StringFormatVerification/fail_exponent.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.fail_exponent --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
TG-2897

‎jbmc/regression/jbmc-strings/StringFormatVerification/fail_exponent_float_arg.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.fail_exponent --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
TG-2532

‎jbmc/regression/jbmc-strings/StringFormatVerification/fail_exponent_uppercase.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.fail_exponent_uppercase --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
TG-2897

‎jbmc/regression/jbmc-strings/StringFormatVerification/fail_float.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
test.class
3+
--max-nondet-string-length 20 --function test.fail_float --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
--
9+
TG-2897

0 commit comments

Comments
 (0)