Made allocations involving sizeof work correctly (test/malloc.c).

[splint.git] / test / compdestroy.expect

diff --git a/test/compdestroy.expect b/test/compdestroy.expect
index 9e05b62a266cf7c2e4f8f066974a49f283878f38..6f344765534519aa8e31fda6da24c75337e7c1d8 100644 (file)
--- a/test/compdestroy.expect
+++ b/test/compdestroy.expect
@@ -32,8 +32,13 @@ compdestroy.c:16:13: Possibly dead storage x->ips[] passed as out parameter:
    compdestroy.c:15:13: Storage x->ips[] possibly released
 compdestroy.c:19:9: Only storage x->ips[] (type oip) derived from released
                        storage may not have been released: x->ips
+compdestroy.c:15:13: Possible out-of-bounds read: x->ips[i]
+    Unable to resolve constraint:
+    requires maxRead(x->ips @ compdestroy.c:15:13) >= i @ compdestroy.c:15:20
+     needed to satisfy precondition:
+    requires maxRead(x->ips @ compdestroy.c:15:13) >= i @ compdestroy.c:15:20
 compdestroy.c: (in function sip_free2)
 compdestroy.c:25:9: Only storage *(x->ips) (type oip) derived from released
                        storage is not released (memory leak): x->ips
 
-Finished checking --- 3 code warnings, as expected
+Finished checking --- 4 code warnings, as expected