[Instantiate] m/c alloc: refuse incomplete types

src/plugins/instantiate/stdlib/calloc.ml

@@ -133,7 +133,8 @@ let well_typed_call ret args =
   match ret, args with
   | Some ret, [ _ ; _ ] ->
     let t = Cil.typeOfLval ret in
-    Cil.isPointerType t && not (Cil.isVoidPtrType t)
+    Cil.isPointerType t && not (Cil.isVoidPtrType t) &&
+    Cil.isCompleteType (Cil.typeOf_pointed t)
   | _ -> false
 
 let key_from_call ret _ =

src/plugins/instantiate/stdlib/malloc.ml

@@ -72,7 +72,8 @@ let well_typed_call ret args =
   match ret, args with
   | Some ret, [ _ ] ->
     let t = Cil.typeOfLval ret in
-    Cil.isPointerType t && not (Cil.isVoidPtrType t)
+    Cil.isPointerType t && not (Cil.isVoidPtrType t) &&
+    Cil.isCompleteType (Cil.typeOf_pointed t)
   | _ -> false
 
 let key_from_call ret _ =

src/plugins/instantiate/tests/stdlib/calloc.c

@@ -19,4 +19,5 @@ int main(void){
   int (*pa) [10] = calloc(10, sizeof(int[10])) ;
   struct Flex* f = calloc(1, sizeof(struct Flex) + 3 * sizeof(int)) ;
   void *v = calloc(10, sizeof(char));
+  struct incomplete* inc = calloc(10, 10);
 }
\ No newline at end of file

src/plugins/instantiate/tests/stdlib/free.c

@@ -11,4 +11,7 @@ void baz(int (*x) [10]){
 }
 void with_void(void * x){
   free(x);
+}
+void with_incomplete(struct incomplete* t){
+  free(t);
 }
\ No newline at end of file

src/plugins/instantiate/tests/stdlib/malloc.c

@@ -11,6 +11,8 @@ struct Flex {
   int f[] ;
 } ;
 
+struct incomplete ;
+
 int main(void){
   int* pi = malloc(sizeof(int) * 10) ;
   float* pf = malloc(sizeof(float) * 10) ;
@@ -19,4 +21,5 @@ int main(void){
   int (*pa) [10] = malloc(sizeof(int[10]) * 10) ;
   struct Flex* f = malloc(sizeof(struct Flex) + 3 * sizeof(int)) ;
   void *v = malloc(sizeof(char) * 10);
+  struct incomplete* inc = malloc(10);
 }
\ No newline at end of file

src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle

 [kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
 [instantiate] tests/stdlib/calloc.c:21: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/calloc.c:22: Warning: Ignore call: not well typed
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct X {
@@ -11,6 +12,7 @@ struct Flex {
    char c ;
    int f[] ;
 };
+struct incomplete;
 /*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
     requires only_one: num ≡ 1;
     assigns \result, __fc_heap_status;
@@ -263,6 +265,7 @@ int main(void)
     calloc_st_Flex((unsigned int)1,
                    sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
   void *v = calloc((unsigned int)10,sizeof(char));
+  struct incomplete *inc = calloc((unsigned int)10,(unsigned int)10);
   __retres = 0;
   return __retres;
 }
@@ -271,7 +274,7 @@ int main(void)
 [kernel] Parsing tests/stdlib/result/calloc.c (with preprocessing)
 [kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
 [kernel] tests/stdlib/calloc.c:14: Warning: 
-  def'n of func main at tests/stdlib/calloc.c:14 (sum 6403) conflicts with the one at tests/stdlib/result/calloc.c:252 (sum 8177); keeping the one at tests/stdlib/result/calloc.c:252.
+  def'n of func main at tests/stdlib/calloc.c:14 (sum 7290) conflicts with the one at tests/stdlib/result/calloc.c:253 (sum 9064); keeping the one at tests/stdlib/result/calloc.c:253.
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct X {
@@ -283,6 +286,7 @@ struct Flex {
    char c ;
    int f[] ;
 };
+struct incomplete;
 /*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
     requires only_one: num ≡ 1;
     assigns \result, __fc_heap_status;
@@ -539,6 +543,7 @@ int main(void)
     calloc_st_Flex((unsigned int)1,
                    sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
   void *v = calloc((unsigned int)10,sizeof(char));
+  struct incomplete *inc = calloc((unsigned int)10,(unsigned int)10);
   __retres = 0;
   return __retres;
 }

src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle

@@ -2,6 +2,7 @@
 [instantiate] tests/stdlib/free.c:13: Warning: Ignore call: not well typed
 /* Generated by Frama-C */
 #include "stdlib.h"
+struct incomplete;
 /*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
     assigns __fc_heap_status;
     assigns __fc_heap_status \from __fc_heap_status, ptr;
@@ -104,19 +105,54 @@ void with_void(void *x)
   return;
 }
 
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+    assigns __fc_heap_status;
+    assigns __fc_heap_status \from __fc_heap_status, ptr;
+    frees ptr;
+    
+    behavior allocation:
+      assumes ptr ≢ \null;
+      ensures freed: \allocable(ptr);
+      assigns __fc_heap_status;
+      assigns __fc_heap_status \from __fc_heap_status, ptr;
+      frees ptr;
+    
+    behavior no_allocation:
+      assumes ptr ≡ \null;
+      assigns \nothing;
+      allocates \nothing;
+    
+    complete behaviors no_allocation, allocation;
+    disjoint behaviors no_allocation, allocation;
+ */
+void free_st_incomplete(struct incomplete *ptr)
+{
+  free((void *)ptr);
+  return;
+}
+
+void with_incomplete(struct incomplete *t)
+{
+  free_st_incomplete(t);
+  return;
+}
+
 
 [kernel] Parsing tests/stdlib/result/free.c (with preprocessing)
 [kernel] Parsing tests/stdlib/free.c (with preprocessing)
 [kernel] tests/stdlib/free.c:3: Warning: 
-  dropping duplicate def'n of func foo at tests/stdlib/free.c:3 in favor of that at tests/stdlib/result/free.c:29
+  dropping duplicate def'n of func foo at tests/stdlib/free.c:3 in favor of that at tests/stdlib/result/free.c:30
 [kernel] tests/stdlib/free.c:6: Warning: 
-  dropping duplicate def'n of func bar at tests/stdlib/free.c:6 in favor of that at tests/stdlib/result/free.c:61
+  dropping duplicate def'n of func bar at tests/stdlib/free.c:6 in favor of that at tests/stdlib/result/free.c:62
 [kernel] tests/stdlib/free.c:9: Warning: 
-  dropping duplicate def'n of func baz at tests/stdlib/free.c:9 in favor of that at tests/stdlib/result/free.c:93
+  dropping duplicate def'n of func baz at tests/stdlib/free.c:9 in favor of that at tests/stdlib/result/free.c:94
 [kernel] tests/stdlib/free.c:12: Warning: 
-  dropping duplicate def'n of func with_void at tests/stdlib/free.c:12 in favor of that at tests/stdlib/result/free.c:99
+  dropping duplicate def'n of func with_void at tests/stdlib/free.c:12 in favor of that at tests/stdlib/result/free.c:100
+[kernel] tests/stdlib/free.c:15: Warning: 
+  dropping duplicate def'n of func with_incomplete at tests/stdlib/free.c:15 in favor of that at tests/stdlib/result/free.c:132
 /* Generated by Frama-C */
 #include "stdlib.h"
+struct incomplete;
 /*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
     assigns __fc_heap_status;
     assigns __fc_heap_status \from __fc_heap_status, ptr;
@@ -219,4 +255,36 @@ void with_void(void *x)
   return;
 }
 
+/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
+    assigns __fc_heap_status;
+    assigns __fc_heap_status \from __fc_heap_status, ptr;
+    frees ptr;
+    
+    behavior allocation:
+      assumes ptr ≢ \null;
+      ensures freed: \allocable(\old(ptr));
+      assigns __fc_heap_status;
+      assigns __fc_heap_status \from __fc_heap_status, ptr;
+      frees ptr;
+    
+    behavior no_allocation:
+      assumes ptr ≡ \null;
+      assigns \nothing;
+      allocates \nothing;
+    
+    complete behaviors no_allocation, allocation;
+    disjoint behaviors no_allocation, allocation;
+ */
+void free_st_incomplete(struct incomplete *ptr)
+{
+  free((void *)ptr);
+  return;
+}
+
+void with_incomplete(struct incomplete *t)
+{
+  free_st_incomplete(t);
+  return;
+}
+
 

src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle

 [kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
-[instantiate] tests/stdlib/malloc.c:21: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/malloc.c:23: Warning: Ignore call: not well typed
+[instantiate] tests/stdlib/malloc.c:24: Warning: Ignore call: not well typed
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct X {
@@ -11,6 +12,7 @@ struct Flex {
    char c ;
    int f[] ;
 };
+struct incomplete;
 /*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
     assigns \result, __fc_heap_status;
     assigns \result \from __fc_heap_status, size;
@@ -208,6 +210,7 @@ int main(void)
   struct Flex *f =
     malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
   void *v = malloc(sizeof(char) * (unsigned int)10);
+  struct incomplete *inc = malloc((unsigned int)10);
   __retres = 0;
   return __retres;
 }
@@ -215,8 +218,8 @@ int main(void)
 
 [kernel] Parsing tests/stdlib/result/malloc.c (with preprocessing)
 [kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
-[kernel] tests/stdlib/malloc.c:14: Warning: 
-  def'n of func main at tests/stdlib/malloc.c:14 (sum 6403) conflicts with the one at tests/stdlib/result/malloc.c:198 (sum 8177); keeping the one at tests/stdlib/result/malloc.c:198.
+[kernel] tests/stdlib/malloc.c:16: Warning: 
+  def'n of func main at tests/stdlib/malloc.c:16 (sum 7290) conflicts with the one at tests/stdlib/result/malloc.c:199 (sum 9064); keeping the one at tests/stdlib/result/malloc.c:199.
 /* Generated by Frama-C */
 #include "stdlib.h"
 struct X {
@@ -228,6 +231,7 @@ struct Flex {
    char c ;
    int f[] ;
 };
+struct incomplete;
 /*@ requires correct_size: 0 ≤ size - 8 ∧ 0 ≡ (size - 8) % 4;
     assigns \result, __fc_heap_status;
     assigns \result \from __fc_heap_status, size;
@@ -425,6 +429,7 @@ int main(void)
   struct Flex *f =
     malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
   void *v = malloc(sizeof(char) * (unsigned int)10);
+  struct incomplete *inc = malloc((unsigned int)10);
   __retres = 0;
   return __retres;
 }