Skip to content

Commit 4324bbd

Browse files
committed
Disable warnings that result from array-of with zero length
1 parent eed0afb commit 4324bbd

File tree

3 files changed

+6
-0
lines changed

3 files changed

+6
-0
lines changed

regression/cbmc-java/NondetArray2/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,6 @@ NondetArray2.class
33
--function NondetArray2.main --unwind 5
44
^VERIFICATION SUCCESSFUL$
55
--
6+
--
7+
Disabled pending fixing warnings for array-of with zero length:
68
^warning: ignoring

regression/cbmc-java/NondetArray3/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,6 @@ NondetArray3.class
33
--function NondetArray3.main --unwind 5
44
^VERIFICATION SUCCESSFUL$
55
--
6+
--
7+
Disabled pending fixing warnings for array-of with zero length:
68
^warning: ignoring

regression/cbmc-java/NondetGenericArray/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,6 @@ NondetGenericArray.class
33
--function NondetGenericArray.main
44
^VERIFICATION SUCCESSFUL$
55
--
6+
--
7+
Disabled pending fixing warnings for array-of with zero length:
68
^warning: ignoring

0 commit comments

Comments
 (0)