]> andersk Git - splint.git/blobdiff - test/compdestroy.expect
Made allocations involving sizeof work correctly (test/malloc.c).
[splint.git] / test / compdestroy.expect
index 6c0cdd2ee46dba30a754e958cad566a6453f4505..6f344765534519aa8e31fda6da24c75337e7c1d8 100644 (file)
@@ -17,7 +17,7 @@ Finished checking --- 2 code warnings, as expected
 compdestroy.c: (in function sip_free)
 compdestroy.c:16:13: Possibly dead storage x->ips[] passed as out parameter:
                         x->ips[i]
-   compdestroy.c:15:13: Storage x->ips[] becomes probably dead
+   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: (in function sip_free2)
@@ -29,11 +29,16 @@ Finished checking --- 3 code warnings, as expected
 compdestroy.c: (in function sip_free)
 compdestroy.c:16:13: Possibly dead storage x->ips[] passed as out parameter:
                         x->ips[i]
-   compdestroy.c:15:13: Storage x->ips[] becomes probably dead
+   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
This page took 0.038554 seconds and 4 git commands to generate.