From c295cee826357d1117a1466afa98c317fac9c1b6 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 24 Oct 2019 11:29:48 +0200
Subject: [PATCH] [Builtin] Reject calls with void* input
---
src/plugins/builtin/stdlib/calloc.ml | 4 +-
src/plugins/builtin/stdlib/free.ml | 4 +-
src/plugins/builtin/stdlib/malloc.ml | 4 +-
src/plugins/builtin/string/memcmp.ml | 3 +-
src/plugins/builtin/string/memcpy.ml | 3 +-
src/plugins/builtin/string/memmove.ml | 3 +-
src/plugins/builtin/string/memset.ml | 1 +
src/plugins/builtin/tests/stdlib/calloc.c | 3 +-
src/plugins/builtin/tests/stdlib/free.c | 3 +
src/plugins/builtin/tests/stdlib/malloc.c | 3 +-
.../tests/stdlib/oracle/calloc.res.oracle | 5 +-
.../tests/stdlib/oracle/free.res.oracle | 15 +++++
.../tests/stdlib/oracle/malloc.res.oracle | 5 +-
src/plugins/builtin/tests/string/memcmp.c | 24 ++++----
src/plugins/builtin/tests/string/memcpy.c | 5 ++
src/plugins/builtin/tests/string/memmove.c | 5 ++
src/plugins/builtin/tests/string/memset_0.c | 5 ++
src/plugins/builtin/tests/string/memset_FF.c | 5 ++
.../builtin/tests/string/memset_value.c | 5 ++
.../tests/string/oracle/memcmp.res.oracle | 57 ++++++++++++-------
.../tests/string/oracle/memcpy.res.oracle | 18 ++++++
.../tests/string/oracle/memmove.res.oracle | 18 ++++++
.../tests/string/oracle/memset_0.res.oracle | 18 ++++++
.../tests/string/oracle/memset_FF.res.oracle | 18 ++++++
.../string/oracle/memset_value.res.oracle | 18 ++++++
25 files changed, 210 insertions(+), 42 deletions(-)
diff --git a/src/plugins/builtin/stdlib/calloc.ml b/src/plugins/builtin/stdlib/calloc.ml
index 10ba0682d7a..1f0b3cf9760 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 e654bea033f..4a0e106edda 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 a696a6f6af1..e206b2bdcc8 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 b6052d003d2..bfda47316ec 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 c69f8761334..6c450e5e59c 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 e0445c020be..d4b87f7f288 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 9be7f29ca81..1f6d3d09e67 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 58286c59dda..77be4d292f1 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 eb0ff860035..40cab4f547c 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 e39f5d9c638..0d5aa4ea04a 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 e3e9e4bc0c8..e116acefd06 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 425d46815eb..830b23cefbf 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 bc6d992efeb..c552df1af72 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 8a0b48622a6..004f004f222 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 ed3022f3718..4f245bbbd06 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 3944ba03563..9fca890b0e1 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 f48d1f907dd..ffd73cad6a7 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 33a6c39db64..17c8260b516 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 313df4a29c3..25f04a59ff0 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 646b873e44c..1e239406f5d 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 4a9d9e029c0..b0d5a8eaba6 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 b85ede266e4..75ff285878b 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 5dcae838d7d..ecaeedab7db 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 bc10dec771d..a50c0bf600c 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 e63b609e65b..d7e37edb76c 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;
+}
+
--
GitLab