diff --git a/src/plugins/instantiate/stdlib/calloc.ml b/src/plugins/instantiate/stdlib/calloc.ml
index 1ea994392c6c840d0e183a6db74bf9d53e4f2fc3..e1cc1460c39e452c98b47d1bda2242cdd9f8c935 100644
--- a/src/plugins/instantiate/stdlib/calloc.ml
+++ b/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 _ =
diff --git a/src/plugins/instantiate/stdlib/malloc.ml b/src/plugins/instantiate/stdlib/malloc.ml
index a6debf251e1080313e96210b5a0ecc0404fa29b9..9cc215a771177f55854232557d1d5df6a93e681f 100644
--- a/src/plugins/instantiate/stdlib/malloc.ml
+++ b/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 _ =
diff --git a/src/plugins/instantiate/tests/stdlib/calloc.c b/src/plugins/instantiate/tests/stdlib/calloc.c
index 77be4d292f1d7befca278b4210ea6335c805fed1..87b1f9338ccb5ecdd99d339551a383459f8305bc 100644
--- a/src/plugins/instantiate/tests/stdlib/calloc.c
+++ b/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
diff --git a/src/plugins/instantiate/tests/stdlib/free.c b/src/plugins/instantiate/tests/stdlib/free.c
index 40cab4f547cfcf9ab66b7e278c3a0cce9ddd6c00..e61ed8864c1d2657e6dc1f65a0d047735b3a2d6b 100644
--- a/src/plugins/instantiate/tests/stdlib/free.c
+++ b/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
diff --git a/src/plugins/instantiate/tests/stdlib/malloc.c b/src/plugins/instantiate/tests/stdlib/malloc.c
index 0d5aa4ea04a70e739cf3a4b5e5125baf2b2b1197..00a07820a9ac4377c39826e16538d62e6f8c2322 100644
--- a/src/plugins/instantiate/tests/stdlib/malloc.c
+++ b/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
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
index 5fb370ab29a192623a74034cbf0923e31191b163..81cf9b246df3d570b24e87e36cf0e0e11c4019f3 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle
@@ -1,5 +1,6 @@
 [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;
 }
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
index 1e764fcd7c62f75f1a4160cd430d760db327f29a..11f5ef65b0eda0f0b4f850b39e7595246a5cc234 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle
+++ b/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;
+}
+
 
diff --git a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
index feb0c41909dd4a6cb6b7de4c4ec3dac49cd07869..485abcec7f4dbb6805bd76a022af060cb23a0804 100644
--- a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
+++ b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle
@@ -1,5 +1,6 @@
 [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;
 }