diff --git a/src/plugins/instantiate/tests/string/memcmp.c b/src/plugins/instantiate/tests/string/memcmp.c index 404692f9eb118b24ffa7716dceb72b990d973d2e..d8d958e45ed65cd76e23e500c531d6f498ab8c88 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 f2c6c03d864470e963082de31044b103dde3a930..fda5fadb75810c7a18c2549b8541046d80c68d79 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 a40698297fd597433f1ced51585f2c1176b285f7..72a5e891aeeffcfa3ec18fc5cbf372aa43734916 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 f87d862900577f5b3f9047f1f3c3df7c7fbfe9b1..bb58f3d9c3af3350257485bb6242ba931f89da4b 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 45b8e49cd11a595270606364836e897a89ba3c73..68f3253fc58737341f77805794f8a567b6d000ed 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 654466dbc2f9ee2777f40c0935494700e7b82649..ad966713db9b11cef6c1ed3941f92062589730d1 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 18ada799c0a1e0f5e274988851be469c4bc793bc..856300f9ad02c6ada927f4ccc39d1f04c436be7b 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 78076d88eb1a02608bcc45fddb4e91962634940c..35a4b88ca8fc95e3b60b3bd9ab6af8c41c3a50d3 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 15c80507c4a17b1b2c366d5ce5cccfacb4008a46..b53227bdabf4910160b6a2ba74c014ef788e3ea5 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 368076b562a058ace4515686e79749ec84e3ebcc..af6a60f7c80cf3156dafa841eacb02efbb0e2002 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 0054f34057790f9241827f2bf1e3f767e6404bd3..91a1e42f767e8b671d559e1c81df16766352659e 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 f68d49c8e424bb07a8256d8804001f17aad4fe39..8609a955121da6329d80d472a6c6283008fd558b 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; +} +