diff --git a/src/plugins/builtin/stdlib/calloc.ml b/src/plugins/builtin/stdlib/calloc.ml
index 10ba0682d7ac4938e61c62c0717fe1936ec00a3b..1f0b3cf976049d0b81be1358f5f2eb6b03d20a74 100644
--- a/src/plugins/builtin/stdlib/calloc.ml
+++ b/src/plugins/builtin/stdlib/calloc.ml
@@ -131,7 +131,9 @@ let generate_prototype alloc_type =
let well_typed_call ret args =
match ret, args with
- | Some ret, [ _ ; _ ] -> Cil.isPointerType (Cil.typeOfLval ret)
+ | Some ret, [ _ ; _ ] ->
+ let t = Cil.typeOfLval ret in
+ Cil.isPointerType t && not (Cil.isVoidPtrType t)
| _ -> false
let key_from_call ret _ =
diff --git a/src/plugins/builtin/stdlib/free.ml b/src/plugins/builtin/stdlib/free.ml
index e654bea033f91381c8cf529cf6d77126fc4feee0..4a0e106eddad54daf5adf66c668488c398b4eb52 100644
--- a/src/plugins/builtin/stdlib/free.ml
+++ b/src/plugins/builtin/stdlib/free.ml
@@ -83,7 +83,9 @@ let generate_prototype alloc_t =
let well_typed_call _ret args =
match args with
- | [ ptr ] -> Cil.isPointerType (Cil.typeOf ptr)
+ | [ ptr ] ->
+ let t = Cil.typeOf (Cil.stripCasts ptr) in
+ Cil.isPointerType t && not (Cil.isVoidPtrType t)
| _ -> false
let key_from_call _ret args =
diff --git a/src/plugins/builtin/stdlib/malloc.ml b/src/plugins/builtin/stdlib/malloc.ml
index a696a6f6af1a04a872b8a0e6c2257398caf02809..e206b2bdcc86b707d0aeb832640022d26a7c0855 100644
--- a/src/plugins/builtin/stdlib/malloc.ml
+++ b/src/plugins/builtin/stdlib/malloc.ml
@@ -70,7 +70,9 @@ let generate_prototype alloc_t =
let well_typed_call ret args =
match ret, args with
- | Some ret, [ _ ] -> Cil.isPointerType (Cil.typeOfLval ret)
+ | Some ret, [ _ ] ->
+ let t = Cil.typeOfLval ret in
+ Cil.isPointerType t && not (Cil.isVoidPtrType t)
| _ -> false
let key_from_call ret _ =
diff --git a/src/plugins/builtin/string/memcmp.ml b/src/plugins/builtin/string/memcmp.ml
index b6052d003d2061161a1324d0503015aa50dda9d8..bfda47316ec5b6180f43ba7aa4f533c6ea38082a 100644
--- a/src/plugins/builtin/string/memcmp.ml
+++ b/src/plugins/builtin/string/memcmp.ml
@@ -99,7 +99,8 @@ let type_from_arg x =
let well_typed_call _ret = function
| [ s1 ; s2 ; len ] ->
(Cil.isIntegralType (Cil.typeOf len)) &&
- (Cil_datatype.Typ.equal (type_from_arg s1) (type_from_arg s2))
+ (Cil_datatype.Typ.equal (type_from_arg s1) (type_from_arg s2)) &&
+ (not (Cil.isVoidType (type_from_arg s1)))
| _ -> false
let key_from_call _ret = function
diff --git a/src/plugins/builtin/string/memcpy.ml b/src/plugins/builtin/string/memcpy.ml
index c69f8761334799d4a196f90e43a5f9ed1bd039fe..6c450e5e59c5981585fa5a815c8ce344cf75f44d 100644
--- a/src/plugins/builtin/string/memcpy.ml
+++ b/src/plugins/builtin/string/memcpy.ml
@@ -105,7 +105,8 @@ let type_from_arg x =
let well_typed_call _ret = function
| [ dest ; src ; len ] ->
(Cil.isIntegralType (Cil.typeOf len)) &&
- (Cil_datatype.Typ.equal (type_from_arg dest) (type_from_arg src))
+ (Cil_datatype.Typ.equal (type_from_arg dest) (type_from_arg src)) &&
+ (not (Cil.isVoidType (type_from_arg dest)))
| _ -> false
let key_from_call _ret = function
diff --git a/src/plugins/builtin/string/memmove.ml b/src/plugins/builtin/string/memmove.ml
index e0445c020be4d4e6e4165fc6613fe98ac19be164..d4b87f7f28818db33b47052bbed063acab7370af 100644
--- a/src/plugins/builtin/string/memmove.ml
+++ b/src/plugins/builtin/string/memmove.ml
@@ -99,7 +99,8 @@ let type_from_arg x =
let well_typed_call _ret = function
| [ dest ; src ; len ] ->
(Cil.isIntegralType (Cil.typeOf len)) &&
- (Cil_datatype.Typ.equal (type_from_arg dest) (type_from_arg src))
+ (Cil_datatype.Typ.equal (type_from_arg dest) (type_from_arg src)) &&
+ (not (Cil.isVoidType (type_from_arg dest)))
| _ -> false
let key_from_call _ret = function
diff --git a/src/plugins/builtin/string/memset.ml b/src/plugins/builtin/string/memset.ml
index 9be7f29ca81c29cecc8e6ac66aee806a2ba7912b..1f6d3d09e67a6e5a83d7fcb13056fda9ad85197e 100644
--- a/src/plugins/builtin/string/memset.ml
+++ b/src/plugins/builtin/string/memset.ml
@@ -190,6 +190,7 @@ let is_union_type = function
let well_typed_call _ret = function
| [ ptr ; _ ; _ ] when any_char_composed_type (type_from_arg ptr) -> true
| [ ptr ; _ ; _ ] when is_union_type (type_from_arg ptr) -> false
+ | [ ptr ; _ ; _ ] when Cil.isVoidType (type_from_arg ptr) -> false
| [ _ ; value ; _ ] ->
begin match memset_value value with
| None -> false
diff --git a/src/plugins/builtin/tests/stdlib/calloc.c b/src/plugins/builtin/tests/stdlib/calloc.c
index 58286c59dda33f8d286a1963f9c6b54e846fc339..77be4d292f1d7befca278b4210ea6335c805fed1 100644
--- a/src/plugins/builtin/tests/stdlib/calloc.c
+++ b/src/plugins/builtin/tests/stdlib/calloc.c
@@ -16,8 +16,7 @@ int main(void){
float* pf = calloc(10, sizeof(float)) ;
struct X* px = calloc(10, sizeof(struct X)) ;
char* pc = calloc(10, sizeof(char)) ;
-
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));
}
\ No newline at end of file
diff --git a/src/plugins/builtin/tests/stdlib/free.c b/src/plugins/builtin/tests/stdlib/free.c
index eb0ff8600352d0596a373bd47f4176c6f4b03515..40cab4f547cfcf9ab66b7e278c3a0cce9ddd6c00 100644
--- a/src/plugins/builtin/tests/stdlib/free.c
+++ b/src/plugins/builtin/tests/stdlib/free.c
@@ -8,4 +8,7 @@ void bar(float * x){
}
void baz(int (*x) [10]){
free(x);
+}
+void with_void(void * x){
+ free(x);
}
\ No newline at end of file
diff --git a/src/plugins/builtin/tests/stdlib/malloc.c b/src/plugins/builtin/tests/stdlib/malloc.c
index e39f5d9c638185daf075df32f5ba517c914c57d2..0d5aa4ea04a70e739cf3a4b5e5125baf2b2b1197 100644
--- a/src/plugins/builtin/tests/stdlib/malloc.c
+++ b/src/plugins/builtin/tests/stdlib/malloc.c
@@ -16,8 +16,7 @@ int main(void){
float* pf = malloc(sizeof(float) * 10) ;
struct X* px = malloc(sizeof(struct X) * 10) ;
char* pc = malloc(10) ;
-
int (*pa) [10] = malloc(sizeof(int[10]) * 10) ;
-
struct Flex* f = malloc(sizeof(struct Flex) + 3 * sizeof(int)) ;
+ void *v = malloc(sizeof(char) * 10);
}
\ No newline at end of file
diff --git a/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle
index e3e9e4bc0c832401cbe2bca9a9c3680110c641ac..e116acefd063d05eade55186370bdd08e8660c73 100644
--- a/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle
+++ b/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing tests/stdlib/calloc.c (with preprocessing)
+[builtin] tests/stdlib/calloc.c:21: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -261,6 +262,7 @@ int main(void)
struct Flex *f =
calloc_Flex((unsigned int)1,
sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+ void *v = calloc((unsigned int)10,sizeof(char));
__retres = 0;
return __retres;
}
@@ -269,7 +271,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 5516) conflicts with the one at tests/stdlib/result/calloc.c:252 (sum 7290); keeping the one at tests/stdlib/result/calloc.c:252.
+ 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.
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -536,6 +538,7 @@ int main(void)
struct Flex *f =
calloc_Flex((unsigned int)1,
sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+ void *v = calloc((unsigned int)10,sizeof(char));
__retres = 0;
return __retres;
}
diff --git a/src/plugins/builtin/tests/stdlib/oracle/free.res.oracle b/src/plugins/builtin/tests/stdlib/oracle/free.res.oracle
index 425d46815eb161fde0fb87e00a514ee05c7fe745..830b23cefbf2e40ca1717eef885baa42ed5255f0 100644
--- a/src/plugins/builtin/tests/stdlib/oracle/free.res.oracle
+++ b/src/plugins/builtin/tests/stdlib/oracle/free.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing tests/stdlib/free.c (with preprocessing)
+[builtin] tests/stdlib/free.c:13: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
@@ -97,6 +98,12 @@ void baz(int (*x)[10])
return;
}
+void with_void(void *x)
+{
+ free(x);
+ return;
+}
+
[kernel] Parsing tests/stdlib/result/free.c (with preprocessing)
[kernel] Parsing tests/stdlib/free.c (with preprocessing)
@@ -106,6 +113,8 @@ void baz(int (*x)[10])
dropping duplicate def'n of func bar at tests/stdlib/free.c:6 in favor of that at tests/stdlib/result/free.c:61
[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
+[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
/* Generated by Frama-C */
#include "stdlib.h"
/*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr);
@@ -204,4 +213,10 @@ void baz(int (*x)[10])
return;
}
+void with_void(void *x)
+{
+ free(x);
+ return;
+}
+
diff --git a/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle
index bc6d992efebc1b0ad07ae6892793b2cad5e58506..c552df1af72cb64eb21433d37f1bcae2cdd66583 100644
--- a/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle
+++ b/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing tests/stdlib/malloc.c (with preprocessing)
+[builtin] tests/stdlib/malloc.c:21: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -206,6 +207,7 @@ int main(void)
int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
struct Flex *f =
malloc_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+ void *v = malloc(sizeof(char) * (unsigned int)10);
__retres = 0;
return __retres;
}
@@ -214,7 +216,7 @@ 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 5516) conflicts with the one at tests/stdlib/result/malloc.c:198 (sum 7290); keeping the one at tests/stdlib/result/malloc.c:198.
+ 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.
/* Generated by Frama-C */
#include "stdlib.h"
struct X {
@@ -422,6 +424,7 @@ int main(void)
int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
struct Flex *f =
malloc_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+ void *v = malloc(sizeof(char) * (unsigned int)10);
__retres = 0;
return __retres;
}
diff --git a/src/plugins/builtin/tests/string/memcmp.c b/src/plugins/builtin/tests/string/memcmp.c
index 8a0b48622a604a70d577c4c8d85abe847214e98e..004f004f222223440c8a3221832d494ecd8541ce 100644
--- a/src/plugins/builtin/tests/string/memcmp.c
+++ b/src/plugins/builtin/tests/string/memcmp.c
@@ -7,22 +7,26 @@ struct X {
typedef int named ;
-int integer(int src[10], int dest[10]){
- return memcmp(dest, src, 10 * sizeof(int));
+int integer(int s1[10], int s2[10]){
+ return memcmp(s1, s2, 10 * sizeof(int));
}
-int with_named(named src[10], named dest[10]){
- return memcmp(dest, src, 10 * sizeof(named));
+int with_named(named s1[10], named s2[10]){
+ return memcmp(s1, s2, 10 * sizeof(named));
}
-int structure(struct X src[10], struct X dest[10]){
- return memcmp(dest, src, 10 * sizeof(struct X));
+int structure(struct X s1[10], struct X s2[10]){
+ return memcmp(s1, s2, 10 * sizeof(struct X));
}
-int pointers(int* src[10], int* dest[10]){
- return memcmp(dest, src, 10 * sizeof(int*));
+int pointers(int* s1[10], int* s2[10]){
+ return memcmp(s1, s2, 10 * sizeof(int*));
}
-int nested(int (*src)[10], int (*dest)[10], int n){
- return memcmp(dest, src, n * sizeof(int[10]));
+int nested(int (*s1)[10], int (*s2)[10], int n){
+ return memcmp(s1, s2, n * sizeof(int[10]));
}
+
+int with_void(void *s1, void *s2, int n){
+ return memcmp(s1, s2, 10) ;
+}
\ No newline at end of file
diff --git a/src/plugins/builtin/tests/string/memcpy.c b/src/plugins/builtin/tests/string/memcpy.c
index ed3022f37184cd9cb47a4029525c9407e2040348..4f245bbbd068b03d854f4dbf7571693be07af82f 100644
--- a/src/plugins/builtin/tests/string/memcpy.c
+++ b/src/plugins/builtin/tests/string/memcpy.c
@@ -31,3 +31,8 @@ void nested(int (*src)[10], int (*dest)[10], int n){
int (*res) [10] = memcpy(dest, src, n * sizeof(int[10]));
memcpy(src, res, n * sizeof(int[10]));
}
+
+void with_void(void *src, void *dest, int n){
+ void *res = memcpy(dest, src, n);
+ memcpy(src, res, n);
+}
diff --git a/src/plugins/builtin/tests/string/memmove.c b/src/plugins/builtin/tests/string/memmove.c
index 3944ba0356393d9c72b479a4e4cdc29011027d40..9fca890b0e18cd35a23f399ee9bf2d86262e6e65 100644
--- a/src/plugins/builtin/tests/string/memmove.c
+++ b/src/plugins/builtin/tests/string/memmove.c
@@ -31,3 +31,8 @@ void nested(int (*src)[10], int (*dest)[10], int n){
int (*res) [10] = memmove(dest, src, n * sizeof(int[10]));
memmove(src, res, n * sizeof(int[10]));
}
+
+void with_void(void *src, void *dest, int n){
+ void *res = memmove(dest, src, n);
+ memmove(src, res, n);
+}
diff --git a/src/plugins/builtin/tests/string/memset_0.c b/src/plugins/builtin/tests/string/memset_0.c
index f48d1f907dd86fed8aee2d96354310886f7c8111..ffd73cad6a70f0b48b2e47fa34756d3a982456b3 100644
--- a/src/plugins/builtin/tests/string/memset_0.c
+++ b/src/plugins/builtin/tests/string/memset_0.c
@@ -51,3 +51,8 @@ void nested(int (*dest)[10], int n){
int (*res) [10] = memset(dest, 0, n * sizeof(int[10]));
memset(res, 0, n * sizeof(int[10]));
}
+
+void with_void(void* dest){
+ void* res = memset(dest, 0, 10);
+ memset(res, 0, 10);
+}
diff --git a/src/plugins/builtin/tests/string/memset_FF.c b/src/plugins/builtin/tests/string/memset_FF.c
index 33a6c39db6470fe89253697e595a3dc81b2b581c..17c8260b5165b3f8b6ff0fdfd04a2c5c4eabc653 100644
--- a/src/plugins/builtin/tests/string/memset_FF.c
+++ b/src/plugins/builtin/tests/string/memset_FF.c
@@ -77,3 +77,8 @@ void nested(int (*dest)[10], int n){
int (*res) [10] = memset(dest, 0xFF, n * sizeof(int[10]));
memset(res, 0xFF, n * sizeof(int[10]));
}
+
+void with_void(void* dest){
+ void* res = memset(dest, 0xFF, 10);
+ memset(res, 0xFF, 10);
+}
diff --git a/src/plugins/builtin/tests/string/memset_value.c b/src/plugins/builtin/tests/string/memset_value.c
index 313df4a29c325ac4631efc64db9beefb24639df6..25f04a59ff02c4378a30f44a82d1ffa81758f895 100644
--- a/src/plugins/builtin/tests/string/memset_value.c
+++ b/src/plugins/builtin/tests/string/memset_value.c
@@ -46,3 +46,8 @@ void nested(int (*dest)[10], int n, int value){
int (*res) [10] = memset(dest, value, n * sizeof(int[10]));
memset(res, value, n * sizeof(int[10]));
}
+
+void with_void(void* dest, int value){
+ void* res = memset(dest, value, 10);
+ memset(res, value, 10);
+}
diff --git a/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle b/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle
index 646b873e44cdacc2c02d7405e20ce67f34e1619c..1e239406f5d277825d1cf5932e8da3a9510ecd81 100644
--- a/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing tests/string/memcmp.c (with preprocessing)
+[builtin] tests/string/memcmp.c:31: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -32,17 +33,17 @@ int memcmp_int(int const *s1, int const *s2, size_t len)
return __retres;
}
-int integer(int * /*[10]*/ src, int * /*[10]*/ dest)
+int integer(int * /*[10]*/ s1, int * /*[10]*/ s2)
{
int tmp;
- tmp = memcmp_int(dest,src,(unsigned int)10 * sizeof(int));
+ tmp = memcmp_int(s1,s2,(unsigned int)10 * sizeof(int));
return tmp;
}
-int with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
+int with_named(named * /*[10]*/ s1, named * /*[10]*/ s2)
{
int tmp;
- tmp = memcmp_int(dest,src,(unsigned int)10 * sizeof(named));
+ tmp = memcmp_int(s1,s2,(unsigned int)10 * sizeof(named));
return tmp;
}
@@ -70,10 +71,10 @@ int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
return __retres;
}
-int structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
+int structure(struct X * /*[10]*/ s1, struct X * /*[10]*/ s2)
{
int tmp;
- tmp = memcmp_X(dest,src,(unsigned int)10 * sizeof(struct X));
+ tmp = memcmp_X(s1,s2,(unsigned int)10 * sizeof(struct X));
return tmp;
}
@@ -101,10 +102,10 @@ int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
return __retres;
}
-int pointers(int ** /*[10]*/ src, int ** /*[10]*/ dest)
+int pointers(int ** /*[10]*/ s1, int ** /*[10]*/ s2)
{
int tmp;
- tmp = memcmp_ptr_int(dest,src,(unsigned int)10 * sizeof(int *));
+ tmp = memcmp_ptr_int(s1,s2,(unsigned int)10 * sizeof(int *));
return tmp;
}
@@ -135,10 +136,17 @@ int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
return __retres;
}
-int nested(int (*src)[10], int (*dest)[10], int n)
+int nested(int (*s1)[10], int (*s2)[10], int n)
{
int tmp;
- tmp = memcmp_arr10_int(dest,src,(unsigned int)n * sizeof(int [10]));
+ tmp = memcmp_arr10_int(s1,s2,(unsigned int)n * sizeof(int [10]));
+ return tmp;
+}
+
+int with_void(void *s1, void *s2, int n)
+{
+ int tmp;
+ tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)10);
return tmp;
}
@@ -155,6 +163,8 @@ int nested(int (*src)[10], int (*dest)[10], int n)
def'n of func pointers at tests/string/memcmp.c:22 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:103 (sum 1972); keeping the one at tests/string/result/memcmp.c:103.
[kernel] tests/string/memcmp.c:26: Warning:
def'n of func nested at tests/string/memcmp.c:26 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:137 (sum 1974); keeping the one at tests/string/result/memcmp.c:137.
+[kernel] tests/string/memcmp.c:30: Warning:
+ def'n of func with_void at tests/string/memcmp.c:30 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:144 (sum 1974); keeping the one at tests/string/result/memcmp.c:144.
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -189,18 +199,18 @@ int memcmp_int(int const *s1, int const *s2, size_t len)
return __retres;
}
-int integer(int *src, int *dest)
+int integer(int *s1, int *s2)
{
int tmp;
- tmp = memcmp_int((int const *)dest,(int const *)src,
+ tmp = memcmp_int((int const *)s1,(int const *)s2,
(unsigned int)10 * sizeof(int));
return tmp;
}
-int with_named(named *src, named *dest)
+int with_named(named *s1, named *s2)
{
int tmp;
- tmp = memcmp_int((int const *)dest,(int const *)src,
+ tmp = memcmp_int((int const *)s1,(int const *)s2,
(unsigned int)10 * sizeof(named));
return tmp;
}
@@ -230,10 +240,10 @@ int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
return __retres;
}
-int structure(struct X *src, struct X *dest)
+int structure(struct X *s1, struct X *s2)
{
int tmp;
- tmp = memcmp_X((struct X const *)dest,(struct X const *)src,
+ tmp = memcmp_X((struct X const *)s1,(struct X const *)s2,
(unsigned int)10 * sizeof(struct X));
return tmp;
}
@@ -263,10 +273,10 @@ int memcmp_ptr_int(int * const *s1, int * const *s2, size_t len)
return __retres;
}
-int pointers(int **src, int **dest)
+int pointers(int **s1, int **s2)
{
int tmp;
- tmp = memcmp_ptr_int((int * const *)dest,(int * const *)src,
+ tmp = memcmp_ptr_int((int * const *)s1,(int * const *)s2,
(unsigned int)10 * sizeof(int *));
return tmp;
}
@@ -299,12 +309,19 @@ int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
return __retres;
}
-int nested(int (*src)[10], int (*dest)[10], int n)
+int nested(int (*s1)[10], int (*s2)[10], int n)
{
int tmp;
- tmp = memcmp_arr10_int((int const (*)[10])dest,(int const (*)[10])src,
+ tmp = memcmp_arr10_int((int const (*)[10])s1,(int const (*)[10])s2,
(unsigned int)n * sizeof(int [10]));
return tmp;
}
+int with_void(void *s1, void *s2, int n)
+{
+ int tmp;
+ tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)10);
+ return tmp;
+}
+
diff --git a/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle b/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle
index 4a9d9e029c0b5f0489388b072c0867e0ba5f49f1..b0d5a8eaba67a64185950d39b9418a0c2208f7c8 100644
--- a/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing tests/string/memcpy.c (with preprocessing)
+[builtin] tests/string/memcpy.c:36: Warning: Ignore call: not well typed
+[builtin] tests/string/memcpy.c:37: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -153,6 +155,13 @@ void nested(int (*src)[10], int (*dest)[10], int n)
return;
}
+void with_void(void *src, void *dest, int n)
+{
+ void *res = memcpy(dest,(void const *)src,(unsigned int)n);
+ memcpy(src,(void const *)res,(unsigned int)n);
+ return;
+}
+
[kernel] Parsing tests/string/result/memcpy.c (with preprocessing)
[kernel] Parsing tests/string/memcpy.c (with preprocessing)
@@ -166,6 +175,8 @@ void nested(int (*src)[10], int (*dest)[10], int n)
dropping duplicate def'n of func pointers at tests/string/memcpy.c:25 in favor of that at tests/string/result/memcpy.c:109
[kernel] tests/string/memcpy.c:30: Warning:
dropping duplicate def'n of func nested at tests/string/memcpy.c:30 in favor of that at tests/string/result/memcpy.c:147
+[kernel] tests/string/memcpy.c:35: Warning:
+ dropping duplicate def'n of func with_void at tests/string/memcpy.c:35 in favor of that at tests/string/result/memcpy.c:155
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -330,4 +341,11 @@ void nested(int (*src)[10], int (*dest)[10], int n)
return;
}
+void with_void(void *src, void *dest, int n)
+{
+ void *res = memcpy(dest,(void const *)src,(unsigned int)n);
+ memcpy(src,(void const *)res,(unsigned int)n);
+ return;
+}
+
diff --git a/src/plugins/builtin/tests/string/oracle/memmove.res.oracle b/src/plugins/builtin/tests/string/oracle/memmove.res.oracle
index b85ede266e4f6cc8519bc08c84a4abcaf3ebf16d..75ff285878b4f362ef4acbc8eb1e0537668fa232 100644
--- a/src/plugins/builtin/tests/string/oracle/memmove.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memmove.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing tests/string/memmove.c (with preprocessing)
+[builtin] tests/string/memmove.c:36: Warning: Ignore call: not well typed
+[builtin] tests/string/memmove.c:37: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -137,6 +139,13 @@ void nested(int (*src)[10], int (*dest)[10], int n)
return;
}
+void with_void(void *src, void *dest, int n)
+{
+ void *res = memmove(dest,(void const *)src,(unsigned int)n);
+ memmove(src,(void const *)res,(unsigned int)n);
+ return;
+}
+
[kernel] Parsing tests/string/result/memmove.c (with preprocessing)
[kernel] Parsing tests/string/memmove.c (with preprocessing)
@@ -150,6 +159,8 @@ void nested(int (*src)[10], int (*dest)[10], int n)
dropping duplicate def'n of func pointers at tests/string/memmove.c:25 in favor of that at tests/string/result/memmove.c:97
[kernel] tests/string/memmove.c:30: Warning:
dropping duplicate def'n of func nested at tests/string/memmove.c:30 in favor of that at tests/string/result/memmove.c:131
+[kernel] tests/string/memmove.c:35: Warning:
+ dropping duplicate def'n of func with_void at tests/string/memmove.c:35 in favor of that at tests/string/result/memmove.c:139
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -298,4 +309,11 @@ void nested(int (*src)[10], int (*dest)[10], int n)
return;
}
+void with_void(void *src, void *dest, int n)
+{
+ void *res = memmove(dest,(void const *)src,(unsigned int)n);
+ memmove(src,(void const *)res,(unsigned int)n);
+ return;
+}
+
diff --git a/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle b/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle
index 5dcae838d7dd04eacab54332a8f43f02dd841cbf..ecaeedab7dbb58993c14f34b8f745c3383210e0e 100644
--- a/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing tests/string/memset_0.c (with preprocessing)
+[builtin] tests/string/memset_0.c:56: Warning: Ignore call: not well typed
+[builtin] tests/string/memset_0.c:57: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -224,6 +226,13 @@ void nested(int (*dest)[10], int n)
return;
}
+void with_void(void *dest)
+{
+ void *res = memset(dest,0,(unsigned int)10);
+ memset(res,0,(unsigned int)10);
+ return;
+}
+
[kernel] Parsing tests/string/result/memset_0.c (with preprocessing)
[kernel] Parsing tests/string/memset_0.c (with preprocessing)
@@ -245,6 +254,8 @@ void nested(int (*dest)[10], int n)
dropping duplicate def'n of func pointers at tests/string/memset_0.c:45 in favor of that at tests/string/result/memset_0.c:190
[kernel] tests/string/memset_0.c:50: Warning:
dropping duplicate def'n of func nested at tests/string/memset_0.c:50 in favor of that at tests/string/result/memset_0.c:218
+[kernel] tests/string/memset_0.c:55: Warning:
+ dropping duplicate def'n of func with_void at tests/string/memset_0.c:55 in favor of that at tests/string/result/memset_0.c:226
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -476,4 +487,11 @@ void nested(int (*dest)[10], int n)
return;
}
+void with_void(void *dest)
+{
+ void *res = memset(dest,0,(unsigned int)10);
+ memset(res,0,(unsigned int)10);
+ return;
+}
+
diff --git a/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle b/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle
index bc10dec771d696148a345a43d2a3159531280b45..a50c0bf600c8d5feaf716cba4aab97b4b417c410 100644
--- a/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing tests/string/memset_FF.c (with preprocessing)
+[builtin] tests/string/memset_FF.c:82: Warning: Ignore call: not well typed
+[builtin] tests/string/memset_FF.c:83: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -362,6 +364,13 @@ void nested(int (*dest)[10], int n)
return;
}
+void with_void(void *dest)
+{
+ void *res = memset(dest,0xFF,(unsigned int)10);
+ memset(res,0xFF,(unsigned int)10);
+ return;
+}
+
[kernel] Parsing tests/string/result/memset_FF.c (with preprocessing)
[kernel] Parsing tests/string/memset_FF.c (with preprocessing)
@@ -393,6 +402,8 @@ void nested(int (*dest)[10], int n)
dropping duplicate def'n of func pointers at tests/string/memset_FF.c:71 in favor of that at tests/string/result/memset_FF.c:328
[kernel] tests/string/memset_FF.c:76: Warning:
dropping duplicate def'n of func nested at tests/string/memset_FF.c:76 in favor of that at tests/string/result/memset_FF.c:356
+[kernel] tests/string/memset_FF.c:81: Warning:
+ dropping duplicate def'n of func with_void at tests/string/memset_FF.c:81 in favor of that at tests/string/result/memset_FF.c:364
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -763,4 +774,11 @@ void nested(int (*dest)[10], int n)
return;
}
+void with_void(void *dest)
+{
+ void *res = memset(dest,0xFF,(unsigned int)10);
+ memset(res,0xFF,(unsigned int)10);
+ return;
+}
+
diff --git a/src/plugins/builtin/tests/string/oracle/memset_value.res.oracle b/src/plugins/builtin/tests/string/oracle/memset_value.res.oracle
index e63b609e65b9a6d11742be01d5bd5093edf28192..d7e37edb76c109cdb7e02468df5babf8b0d8d835 100644
--- a/src/plugins/builtin/tests/string/oracle/memset_value.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memset_value.res.oracle
@@ -9,6 +9,8 @@
[builtin] tests/string/memset_value.c:42: Warning: Ignore call: not well typed
[builtin] tests/string/memset_value.c:46: Warning: Ignore call: not well typed
[builtin] tests/string/memset_value.c:47: Warning: Ignore call: not well typed
+[builtin] tests/string/memset_value.c:51: Warning: Ignore call: not well typed
+[builtin] tests/string/memset_value.c:52: Warning: Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -130,6 +132,13 @@ void nested(int (*dest)[10], int n, int value)
return;
}
+void with_void(void *dest, int value)
+{
+ void *res = memset(dest,value,(unsigned int)10);
+ memset(res,value,(unsigned int)10);
+ return;
+}
+
[kernel] Parsing tests/string/result/memset_value.c (with preprocessing)
[kernel] Parsing tests/string/memset_value.c (with preprocessing)
@@ -149,6 +158,8 @@ void nested(int (*dest)[10], int n, int value)
dropping duplicate def'n of func pointers at tests/string/memset_value.c:40 in favor of that at tests/string/result/memset_value.c:107
[kernel] tests/string/memset_value.c:45: Warning:
dropping duplicate def'n of func nested at tests/string/memset_value.c:45 in favor of that at tests/string/result/memset_value.c:114
+[kernel] tests/string/memset_value.c:50: Warning:
+ dropping duplicate def'n of func with_void at tests/string/memset_value.c:50 in favor of that at tests/string/result/memset_value.c:122
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -275,4 +286,11 @@ void nested(int (*dest)[10], int n, int value)
return;
}
+void with_void(void *dest, int value)
+{
+ void *res = memset(dest,value,(unsigned int)10);
+ memset(res,value,(unsigned int)10);
+ return;
+}
+