From 1b103b96a0b50636144458360922c99bff0ee2fa Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 27 Mar 2020 10:17:36 +0100
Subject: [PATCH] [Instantiate] Test for numeric constant as pointers
---
src/plugins/instantiate/tests/string/memcmp.c | 9 ++++++-
src/plugins/instantiate/tests/string/memcpy.c | 9 ++++++-
.../instantiate/tests/string/memmove.c | 7 +++++
.../instantiate/tests/string/memset_0.c | 5 ++++
.../instantiate/tests/string/memset_FF.c | 5 ++++
.../instantiate/tests/string/memset_value.c | 7 ++++-
.../tests/string/oracle/memcmp.res.oracle | 26 +++++++++++++++++++
.../tests/string/oracle/memcpy.res.oracle | 22 ++++++++++++++++
.../tests/string/oracle/memmove.res.oracle | 22 ++++++++++++++++
.../tests/string/oracle/memset_0.res.oracle | 16 ++++++++++++
.../tests/string/oracle/memset_FF.res.oracle | 16 ++++++++++++
.../string/oracle/memset_value.res.oracle | 18 +++++++++++++
12 files changed, 159 insertions(+), 3 deletions(-)
diff --git a/src/plugins/instantiate/tests/string/memcmp.c b/src/plugins/instantiate/tests/string/memcmp.c
index 404692f9eb1..d8d958e45ed 100644
--- a/src/plugins/instantiate/tests/string/memcmp.c
+++ b/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));
+}
diff --git a/src/plugins/instantiate/tests/string/memcpy.c b/src/plugins/instantiate/tests/string/memcpy.c
index f2c6c03d864..fda5fadb758 100644
--- a/src/plugins/instantiate/tests/string/memcpy.c
+++ b/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));
+}
diff --git a/src/plugins/instantiate/tests/string/memmove.c b/src/plugins/instantiate/tests/string/memmove.c
index a40698297fd..72a5e891aee 100644
--- a/src/plugins/instantiate/tests/string/memmove.c
+++ b/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));
+}
diff --git a/src/plugins/instantiate/tests/string/memset_0.c b/src/plugins/instantiate/tests/string/memset_0.c
index f87d8629005..bb58f3d9c3a 100644
--- a/src/plugins/instantiate/tests/string/memset_0.c
+++ b/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);
+}
diff --git a/src/plugins/instantiate/tests/string/memset_FF.c b/src/plugins/instantiate/tests/string/memset_FF.c
index 45b8e49cd11..68f3253fc58 100644
--- a/src/plugins/instantiate/tests/string/memset_FF.c
+++ b/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);
+}
diff --git a/src/plugins/instantiate/tests/string/memset_value.c b/src/plugins/instantiate/tests/string/memset_value.c
index 654466dbc2f..ad966713db9 100644
--- a/src/plugins/instantiate/tests/string/memset_value.c
+++ b/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);
+}
diff --git a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
index 18ada799c0a..856300f9ad0 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
@@ -1,6 +1,10 @@
[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;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
index 78076d88eb1..35a4b88ca8f 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
+++ b/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;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
index 15c80507c4a..b53227bdabf 100644
--- a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
+++ b/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;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
index 368076b562a..af6a60f7c80 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle
@@ -1,6 +1,8 @@
[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;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
index 0054f340577..91a1e42f767 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle
@@ -1,6 +1,8 @@
[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;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
index f68d49c8e42..8609a955121 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
+++ b/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;
+}
+
--
GitLab