[Instantiate] Test for numeric constant as pointers

src/plugins/instantiate/tests/string/memcmp.c

@@ -34,4 +34,11 @@ int with_void(void *s1, void *s2, int n){
 struct incomplete ;
 int with_incomplete(struct incomplete* s1, struct incomplete* s2, int n){
   return memcmp(s1, s2, n);
-}
+}
\ No newline at end of file
+
+void with_null_or_int(int p[10]){
+  memcmp(NULL, p, 10 * sizeof(int));
+  memcmp(p, NULL, 10 * sizeof(int));
+  memcmp((int const*)42, p, 10 * sizeof(int));
+  memcmp(p, (int const*)42, 10 * sizeof(int));
+}

src/plugins/instantiate/tests/string/memcpy.c

@@ -41,4 +41,11 @@ struct incomplete ;
 void with_incomplete(struct incomplete* src, struct incomplete* dest, int n){
   struct incomplete* res = memcpy(dest, src, n);
   memcpy(src, res, n);
-}
+}
\ No newline at end of file
+
+void with_null_or_int(int p[10]){
+  memcpy(NULL, p, 10 * sizeof(int));
+  memcpy(p, NULL, 10 * sizeof(int));
+  memcpy((int*)42, p, 10 * sizeof(int));
+  memcpy(p, (int*)42, 10 * sizeof(int));
+}

src/plugins/instantiate/tests/string/memmove.c

@@ -42,3 +42,10 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n){
   struct incomplete *res = memmove(dest, src, n);
   memmove(src, res, n);
 }
+
+void with_null_or_int(int p[10]){
+  memmove(NULL, p, 10 * sizeof(int));
+  memmove(p, NULL, 10 * sizeof(int));
+  memmove((int*)42, p, 10 * sizeof(int));
+  memmove(p, (int*)42, 10 * sizeof(int));
+}

src/plugins/instantiate/tests/string/memset_0.c

@@ -62,3 +62,8 @@ void with_void(void* dest){
   void* res = memset(dest, 0, 10);
   memset(res, 0, 10);
 }
+
+void with_null_or_int(void){
+  memset(NULL, 0, 10);
+  memset((int*) 42, 0, 10);
+}

src/plugins/instantiate/tests/string/memset_FF.c

@@ -88,3 +88,8 @@ void with_void(void* dest){
   void* res = memset(dest, 0xFF, 10);
   memset(res, 0xFF, 10);
 }
+
+void with_null_or_int(void){
+  memset(NULL, 0xFF, 10);
+  memset((int*) 42, 0xFF, 10);
+}

src/plugins/instantiate/tests/string/memset_value.c

@@ -61,4 +61,9 @@ void with_void(void* dest, int value){
 void with_incomplete(struct incomplete* dest, int value){
   struct incomplete * res = memset(dest, value, 10);
   memset(res, value, 10);
-}
+}
\ No newline at end of file
+
+void with_null_or_int(int value){
+  memset(NULL, value, 10);
+  memset((int*) 42, value, 10);
+}

src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle

 [kernel] Parsing tests/string/memcmp.c (with preprocessing)
 [instantiate] tests/string/memcmp.c:31: Warning: Ignore call: not well typed
 [instantiate] tests/string/memcmp.c:36: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcmp.c:40: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcmp.c:41: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcmp.c:42: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcmp.c:43: Warning: Ignore call: not well typed
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
@@ -159,6 +163,17 @@ int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
   return tmp;
 }
 
+void with_null_or_int(int * /*[10]*/ p)
+{
+  memcmp((void const *)0,(void const *)p,(unsigned int)10 * sizeof(int));
+  memcmp((void const *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+  memcmp((void const *)((int const *)42),(void const *)p,
+         (unsigned int)10 * sizeof(int));
+  memcmp((void const *)p,(void const *)((int const *)42),
+         (unsigned int)10 * sizeof(int));
+  return;
+}
+
 
 [kernel] Parsing tests/string/result/memcmp.c (with preprocessing)
 /* Generated by Frama-C */
@@ -328,4 +343,15 @@ int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
   return tmp;
 }
 
+void with_null_or_int(int *p)
+{
+  memcmp((void const *)0,(void const *)p,(unsigned int)10 * sizeof(int));
+  memcmp((void const *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+  memcmp((void const *)((int const *)42),(void const *)p,
+         (unsigned int)10 * sizeof(int));
+  memcmp((void const *)p,(void const *)((int const *)42),
+         (unsigned int)10 * sizeof(int));
+  return;
+}
+
 

src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle

@@ -3,6 +3,10 @@
 [instantiate] tests/string/memcpy.c:37: Warning: Ignore call: not well typed
 [instantiate] tests/string/memcpy.c:42: Warning: Ignore call: not well typed
 [instantiate] tests/string/memcpy.c:43: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcpy.c:47: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcpy.c:48: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcpy.c:49: Warning: Ignore call: not well typed
+[instantiate] tests/string/memcpy.c:50: Warning: Ignore call: not well typed
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
@@ -173,6 +177,15 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
   return;
 }
 
+void with_null_or_int(int * /*[10]*/ p)
+{
+  memcpy((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
+  memcpy((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+  memcpy((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
+  memcpy((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+  return;
+}
+
 
 [kernel] Parsing tests/string/result/memcpy.c (with preprocessing)
 /* Generated by Frama-C */
@@ -356,4 +369,13 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
   return;
 }
 
+void with_null_or_int(int *p)
+{
+  memcpy((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
+  memcpy((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+  memcpy((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
+  memcpy((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+  return;
+}
+
 

src/plugins/instantiate/tests/string/oracle/memmove.res.oracle

@@ -3,6 +3,10 @@
 [instantiate] tests/string/memmove.c:37: Warning: Ignore call: not well typed
 [instantiate] tests/string/memmove.c:42: Warning: Ignore call: not well typed
 [instantiate] tests/string/memmove.c:43: Warning: Ignore call: not well typed
+[instantiate] tests/string/memmove.c:47: Warning: Ignore call: not well typed
+[instantiate] tests/string/memmove.c:48: Warning: Ignore call: not well typed
+[instantiate] tests/string/memmove.c:49: Warning: Ignore call: not well typed
+[instantiate] tests/string/memmove.c:50: Warning: Ignore call: not well typed
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
@@ -157,6 +161,15 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
   return;
 }
 
+void with_null_or_int(int * /*[10]*/ p)
+{
+  memmove((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
+  memmove((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+  memmove((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
+  memmove((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+  return;
+}
+
 
 [kernel] Parsing tests/string/result/memmove.c (with preprocessing)
 /* Generated by Frama-C */
@@ -324,4 +337,13 @@ void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
   return;
 }
 
+void with_null_or_int(int *p)
+{
+  memmove((void *)0,(void const *)p,(unsigned int)10 * sizeof(int));
+  memmove((void *)p,(void const *)0,(unsigned int)10 * sizeof(int));
+  memmove((void *)((int *)42),(void const *)p,(unsigned int)10 * sizeof(int));
+  memmove((void *)p,(void const *)((int *)42),(unsigned int)10 * sizeof(int));
+  return;
+}
+
 

src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle

 [kernel] Parsing tests/string/memset_0.c (with preprocessing)
 [instantiate] tests/string/memset_0.c:62: Warning: Ignore call: not well typed
 [instantiate] tests/string/memset_0.c:63: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_0.c:67: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_0.c:68: Warning: Ignore call: not well typed
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
@@ -264,6 +266,13 @@ void with_void(void *dest)
   return;
 }
 
+void with_null_or_int(void)
+{
+  memset((void *)0,0,(unsigned int)10);
+  memset((void *)((int *)42),0,(unsigned int)10);
+  return;
+}
+
 
 [kernel] Parsing tests/string/result/memset_0.c (with preprocessing)
 /* Generated by Frama-C */
@@ -535,4 +544,11 @@ void with_void(void *dest)
   return;
 }
 
+void with_null_or_int(void)
+{
+  memset((void *)0,0,(unsigned int)10);
+  memset((void *)((int *)42),0,(unsigned int)10);
+  return;
+}
+
 

src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle

 [kernel] Parsing tests/string/memset_FF.c (with preprocessing)
 [instantiate] tests/string/memset_FF.c:88: Warning: Ignore call: not well typed
 [instantiate] tests/string/memset_FF.c:89: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_FF.c:93: Warning: Ignore call: not well typed
+[instantiate] tests/string/memset_FF.c:94: Warning: Ignore call: not well typed
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
@@ -401,6 +403,13 @@ void with_void(void *dest)
   return;
 }
 
+void with_null_or_int(void)
+{
+  memset((void *)0,0xFF,(unsigned int)10);
+  memset((void *)((int *)42),0xFF,(unsigned int)10);
+  return;
+}
+
 
 [kernel] Parsing tests/string/result/memset_FF.c (with preprocessing)
 /* Generated by Frama-C */
@@ -811,4 +820,11 @@ void with_void(void *dest)
   return;
 }
 
+void with_null_or_int(void)
+{
+  memset((void *)0,0xFF,(unsigned int)10);
+  memset((void *)((int *)42),0xFF,(unsigned int)10);
+  return;
+}
+
 

src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle

@@ -31,6 +31,10 @@
   Ignore call: not well typed
 [instantiate] tests/string/memset_value.c:63: Warning: 
   Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:67: Warning: 
+  Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:68: Warning: 
+  Ignore call: not well typed
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "string.h"
@@ -179,6 +183,13 @@ void with_incomplete(struct incomplete *dest, int value)
   return;
 }
 
+void with_null_or_int(int value)
+{
+  memset((void *)0,value,(unsigned int)10);
+  memset((void *)((int *)42),value,(unsigned int)10);
+  return;
+}
+
 
 [kernel] Parsing tests/string/result/memset_value.c (with preprocessing)
 /* Generated by Frama-C */
@@ -334,4 +345,11 @@ void with_incomplete(struct incomplete *dest, int value)
   return;
 }
 
+void with_null_or_int(int value)
+{
+  memset((void *)0,value,(unsigned int)10);
+  memset((void *)((int *)42),value,(unsigned int)10);
+  return;
+}
+