X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/16c024b587f5ddc115928d5cca7095508aa208d9..6317f163d6dd13ef058d98c91a6f9eb29a9f87f4:/test/compdestroy.expect

diff --git a/test/compdestroy.expect b/test/compdestroy.expect
index 9e05b62..6f34476 100644
--- 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