X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/ae13359213220016611ceaf93109dac6849be88b..6317f163d6dd13ef058d98c91a6f9eb29a9f87f4:/test/malloc.expect

diff --git a/test/malloc.expect b/test/malloc.expect
new file mode 100644
index 0000000..2bc1196
--- /dev/null
+++ b/test/malloc.expect
@@ -0,0 +1,35 @@
+
+malloc.c: (in function f1)
+malloc.c:3:21: Allocated memory is converted to type int * of (size 32), which
+    is not divisible into original allocation of space for 89 elements of type
+    void * (size 8)
+malloc.c:5:5: Likely out-of-bounds store: ip[88]
+    Unable to resolve constraint:
+    requires 21 >= 88
+     needed to satisfy precondition:
+    requires maxSet(ip @ malloc.c:5:5) >= 88
+malloc.c: (in function f2)
+malloc.c:15:5: Likely out-of-bounds store: ip[22]
+    Unable to resolve constraint:
+    requires 21 >= 22
+     needed to satisfy precondition:
+    requires maxSet(ip @ malloc.c:15:5) >= 22
+malloc.c: (in function f3)
+malloc.c:26:5: Likely out-of-bounds store: ip[87]
+    Unable to resolve constraint:
+    requires 86 >= 87
+     needed to satisfy precondition:
+    requires maxSet(ip @ malloc.c:26:5) >= 87
+malloc.c: (in function f4)
+malloc.c:33:21: Allocated memory is used as a different type (int) from the
+                   sizeof type (short int)
+malloc.c:33:21: Allocated memory is converted to type int * of (size 32), which
+    is not divisible into original allocation of space for 87 elements of type
+    short int (size 8)
+malloc.c:35:5: Likely out-of-bounds store: ip[86]
+    Unable to resolve constraint:
+    requires 20 >= 86
+     needed to satisfy precondition:
+    requires maxSet(ip @ malloc.c:35:5) >= 86
+
+Finished checking --- 7 code warnings, as expected