From a465676c71fb6fd008e6dff2f41c025c69dc25f3 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 25 Mar 2020 18:23:06 +0100
Subject: [PATCH] [Instantiate] Ignore incomplete types in string functions
---
src/plugins/instantiate/string/memcmp.ml | 3 +-
src/plugins/instantiate/string/memcpy.ml | 3 +-
src/plugins/instantiate/string/memmove.ml | 3 +-
src/plugins/instantiate/string/memset.ml | 1 +
src/plugins/instantiate/tests/string/memcmp.c | 5 +++
src/plugins/instantiate/tests/string/memcpy.c | 6 +++
.../instantiate/tests/string/memmove.c | 6 +++
.../instantiate/tests/string/memset_value.c | 5 +++
.../tests/string/oracle/memcmp.res.oracle | 31 +++++++++++---
.../tests/string/oracle/memcpy.res.oracle | 34 +++++++++++++---
.../tests/string/oracle/memmove.res.oracle | 34 +++++++++++++---
.../string/oracle/memset_value.res.oracle | 40 ++++++++++++++-----
12 files changed, 141 insertions(+), 30 deletions(-)
diff --git a/src/plugins/instantiate/string/memcmp.ml b/src/plugins/instantiate/string/memcmp.ml
index 813ab06065f..e493cbb3939 100644
--- a/src/plugins/instantiate/string/memcmp.ml
+++ b/src/plugins/instantiate/string/memcmp.ml
@@ -97,7 +97,8 @@ 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)) &&
- (not (Cil.isVoidType (type_from_arg s1)))
+ (not (Cil.isVoidType (type_from_arg s1))) &&
+ (Cil.isCompleteType (type_from_arg s1))
| _ -> false
let key_from_call _ret = function
diff --git a/src/plugins/instantiate/string/memcpy.ml b/src/plugins/instantiate/string/memcpy.ml
index 6be6f6664ba..02d06b3d5ea 100644
--- a/src/plugins/instantiate/string/memcpy.ml
+++ b/src/plugins/instantiate/string/memcpy.ml
@@ -103,7 +103,8 @@ 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)) &&
- (not (Cil.isVoidType (type_from_arg dest)))
+ (not (Cil.isVoidType (type_from_arg dest))) &&
+ (Cil.isCompleteType (type_from_arg dest))
| _ -> false
let key_from_call _ret = function
diff --git a/src/plugins/instantiate/string/memmove.ml b/src/plugins/instantiate/string/memmove.ml
index 97c3dcb1c57..75aef926971 100644
--- a/src/plugins/instantiate/string/memmove.ml
+++ b/src/plugins/instantiate/string/memmove.ml
@@ -97,7 +97,8 @@ 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)) &&
- (not (Cil.isVoidType (type_from_arg dest)))
+ (not (Cil.isVoidType (type_from_arg dest))) &&
+ (Cil.isCompleteType (type_from_arg dest))
| _ -> false
let key_from_call _ret = function
diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml
index d597bd3a452..79c0fd60bbe 100644
--- a/src/plugins/instantiate/string/memset.ml
+++ b/src/plugins/instantiate/string/memset.ml
@@ -197,6 +197,7 @@ let well_typed_call _ret = function
| [ ptr ; _ ; _ ] when any_char_composed_type (type_from_arg ptr) -> true
| [ ptr ; _ ; _ ] when contains_union_type (type_from_arg ptr) -> false
| [ ptr ; _ ; _ ] when Cil.isVoidType (type_from_arg ptr) -> false
+ | [ ptr ; _ ; _ ] when not (Cil.isCompleteType (type_from_arg ptr)) -> false
| [ _ ; value ; _ ] ->
begin match memset_value value with
| None -> false
diff --git a/src/plugins/instantiate/tests/string/memcmp.c b/src/plugins/instantiate/tests/string/memcmp.c
index 004f004f222..404692f9eb1 100644
--- a/src/plugins/instantiate/tests/string/memcmp.c
+++ b/src/plugins/instantiate/tests/string/memcmp.c
@@ -29,4 +29,9 @@ int nested(int (*s1)[10], int (*s2)[10], int n){
int with_void(void *s1, void *s2, int n){
return memcmp(s1, s2, 10) ;
+}
+
+struct incomplete ;
+int with_incomplete(struct incomplete* s1, struct incomplete* s2, int n){
+ return memcmp(s1, s2, n);
}
\ No newline at end of file
diff --git a/src/plugins/instantiate/tests/string/memcpy.c b/src/plugins/instantiate/tests/string/memcpy.c
index 4f245bbbd06..f2c6c03d864 100644
--- a/src/plugins/instantiate/tests/string/memcpy.c
+++ b/src/plugins/instantiate/tests/string/memcpy.c
@@ -36,3 +36,9 @@ void with_void(void *src, void *dest, int n){
void *res = memcpy(dest, src, n);
memcpy(src, res, n);
}
+
+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
diff --git a/src/plugins/instantiate/tests/string/memmove.c b/src/plugins/instantiate/tests/string/memmove.c
index 9fca890b0e1..a40698297fd 100644
--- a/src/plugins/instantiate/tests/string/memmove.c
+++ b/src/plugins/instantiate/tests/string/memmove.c
@@ -36,3 +36,9 @@ void with_void(void *src, void *dest, int n){
void *res = memmove(dest, src, n);
memmove(src, res, n);
}
+
+struct incomplete ;
+void with_incomplete(struct incomplete *src, struct incomplete *dest, int n){
+ struct incomplete *res = memmove(dest, src, n);
+ memmove(src, res, n);
+}
diff --git a/src/plugins/instantiate/tests/string/memset_value.c b/src/plugins/instantiate/tests/string/memset_value.c
index 25f04a59ff0..432b8ed6a6d 100644
--- a/src/plugins/instantiate/tests/string/memset_value.c
+++ b/src/plugins/instantiate/tests/string/memset_value.c
@@ -51,3 +51,8 @@ void with_void(void* dest, int value){
void* res = memset(dest, value, 10);
memset(res, value, 10);
}
+
+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
diff --git a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
index 9a3d0e63811..9d73f30f20f 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle
@@ -1,5 +1,6 @@
[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
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -9,6 +10,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_read_s1:
@@ -150,21 +152,30 @@ int with_void(void *s1, void *s2, int n)
return tmp;
}
+int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
+{
+ int tmp;
+ tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)n);
+ return tmp;
+}
+
[kernel] Parsing tests/string/result/memcmp.c (with preprocessing)
[kernel] Parsing tests/string/memcmp.c (with preprocessing)
[kernel] tests/string/memcmp.c:10: Warning:
- def'n of func integer at tests/string/memcmp.c:10 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:34 (sum 1972); keeping the one at tests/string/result/memcmp.c:34.
+ def'n of func integer at tests/string/memcmp.c:10 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:35 (sum 1972); keeping the one at tests/string/result/memcmp.c:35.
[kernel] tests/string/memcmp.c:14: Warning:
- def'n of func with_named at tests/string/memcmp.c:14 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:41 (sum 1972); keeping the one at tests/string/result/memcmp.c:41.
+ def'n of func with_named at tests/string/memcmp.c:14 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:42 (sum 1972); keeping the one at tests/string/result/memcmp.c:42.
[kernel] tests/string/memcmp.c:18: Warning:
- def'n of func structure at tests/string/memcmp.c:18 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:72 (sum 1972); keeping the one at tests/string/result/memcmp.c:72.
+ def'n of func structure at tests/string/memcmp.c:18 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:73 (sum 1972); keeping the one at tests/string/result/memcmp.c:73.
[kernel] tests/string/memcmp.c:22: Warning:
- 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.
+ def'n of func pointers at tests/string/memcmp.c:22 (sum 1085) conflicts with the one at tests/string/result/memcmp.c:104 (sum 1972); keeping the one at tests/string/result/memcmp.c:104.
[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.
+ def'n of func nested at tests/string/memcmp.c:26 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:138 (sum 1974); keeping the one at tests/string/result/memcmp.c:138.
[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.
+ def'n of func with_void at tests/string/memcmp.c:30 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:145 (sum 1974); keeping the one at tests/string/result/memcmp.c:145.
+[kernel] tests/string/memcmp.c:35: Warning:
+ def'n of func with_incomplete at tests/string/memcmp.c:35 (sum 1087) conflicts with the one at tests/string/result/memcmp.c:152 (sum 1974); keeping the one at tests/string/result/memcmp.c:152.
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -174,6 +185,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_read_s1:
@@ -324,4 +336,11 @@ int with_void(void *s1, void *s2, int n)
return tmp;
}
+int with_incomplete(struct incomplete *s1, struct incomplete *s2, int n)
+{
+ int tmp;
+ tmp = memcmp((void const *)s1,(void const *)s2,(unsigned int)n);
+ return tmp;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
index 63bd23cf23c..a9bc6101a25 100644
--- a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/string/memcpy.c (with preprocessing)
[instantiate] tests/string/memcpy.c:36: Warning: Ignore call: not well typed
[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
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -10,6 +12,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -162,21 +165,31 @@ void with_void(void *src, void *dest, int n)
return;
}
+void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
+{
+ struct incomplete *res =
+ memcpy((void *)dest,(void const *)src,(unsigned int)n);
+ memcpy((void *)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)
[kernel] tests/string/memcpy.c:10: Warning:
- dropping duplicate def'n of func integer at tests/string/memcpy.c:10 in favor of that at tests/string/result/memcpy.c:36
+ dropping duplicate def'n of func integer at tests/string/memcpy.c:10 in favor of that at tests/string/result/memcpy.c:37
[kernel] tests/string/memcpy.c:15: Warning:
- dropping duplicate def'n of func with_named at tests/string/memcpy.c:15 in favor of that at tests/string/result/memcpy.c:43
+ dropping duplicate def'n of func with_named at tests/string/memcpy.c:15 in favor of that at tests/string/result/memcpy.c:44
[kernel] tests/string/memcpy.c:20: Warning:
- dropping duplicate def'n of func structure at tests/string/memcpy.c:20 in favor of that at tests/string/result/memcpy.c:76
+ dropping duplicate def'n of func structure at tests/string/memcpy.c:20 in favor of that at tests/string/result/memcpy.c:77
[kernel] tests/string/memcpy.c:25: Warning:
- dropping duplicate def'n of func pointers at tests/string/memcpy.c:25 in favor of that at tests/string/result/memcpy.c:109
+ dropping duplicate def'n of func pointers at tests/string/memcpy.c:25 in favor of that at tests/string/result/memcpy.c:110
[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
+ dropping duplicate def'n of func nested at tests/string/memcpy.c:30 in favor of that at tests/string/result/memcpy.c:148
[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
+ dropping duplicate def'n of func with_void at tests/string/memcpy.c:35 in favor of that at tests/string/result/memcpy.c:156
+[kernel] tests/string/memcpy.c:41: Warning:
+ dropping duplicate def'n of func with_incomplete at tests/string/memcpy.c:41 in favor of that at tests/string/result/memcpy.c:163
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -186,6 +199,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -349,4 +363,12 @@ void with_void(void *src, void *dest, int n)
return;
}
+void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
+{
+ struct incomplete *res =
+ memcpy((void *)dest,(void const *)src,(unsigned int)n);
+ memcpy((void *)src,(void const *)res,(unsigned int)n);
+ return;
+}
+
diff --git a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
index 6023a30c6bf..9d8a290eff8 100644
--- a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle
@@ -1,6 +1,8 @@
[kernel] Parsing tests/string/memmove.c (with preprocessing)
[instantiate] tests/string/memmove.c:36: Warning: Ignore call: not well typed
[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
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -10,6 +12,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -146,21 +149,31 @@ void with_void(void *src, void *dest, int n)
return;
}
+void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
+{
+ struct incomplete *res =
+ memmove((void *)dest,(void const *)src,(unsigned int)n);
+ memmove((void *)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)
[kernel] tests/string/memmove.c:10: Warning:
- dropping duplicate def'n of func integer at tests/string/memmove.c:10 in favor of that at tests/string/result/memmove.c:32
+ dropping duplicate def'n of func integer at tests/string/memmove.c:10 in favor of that at tests/string/result/memmove.c:33
[kernel] tests/string/memmove.c:15: Warning:
- dropping duplicate def'n of func with_named at tests/string/memmove.c:15 in favor of that at tests/string/result/memmove.c:39
+ dropping duplicate def'n of func with_named at tests/string/memmove.c:15 in favor of that at tests/string/result/memmove.c:40
[kernel] tests/string/memmove.c:20: Warning:
- dropping duplicate def'n of func structure at tests/string/memmove.c:20 in favor of that at tests/string/result/memmove.c:68
+ dropping duplicate def'n of func structure at tests/string/memmove.c:20 in favor of that at tests/string/result/memmove.c:69
[kernel] tests/string/memmove.c:25: Warning:
- dropping duplicate def'n of func pointers at tests/string/memmove.c:25 in favor of that at tests/string/result/memmove.c:97
+ dropping duplicate def'n of func pointers at tests/string/memmove.c:25 in favor of that at tests/string/result/memmove.c:98
[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
+ dropping duplicate def'n of func nested at tests/string/memmove.c:30 in favor of that at tests/string/result/memmove.c:132
[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
+ dropping duplicate def'n of func with_void at tests/string/memmove.c:35 in favor of that at tests/string/result/memmove.c:140
+[kernel] tests/string/memmove.c:41: Warning:
+ dropping duplicate def'n of func with_incomplete at tests/string/memmove.c:41 in favor of that at tests/string/result/memmove.c:147
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -170,6 +183,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -317,4 +331,12 @@ void with_void(void *src, void *dest, int n)
return;
}
+void with_incomplete(struct incomplete *src, struct incomplete *dest, int n)
+{
+ struct incomplete *res =
+ memmove((void *)dest,(void const *)src,(unsigned int)n);
+ memmove((void *)src,(void const *)res,(unsigned int)n);
+ 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 26ed27864cc..e0a760dc1f0 100644
--- a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
+++ b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle
@@ -23,6 +23,10 @@
Ignore call: not well typed
[instantiate] tests/string/memset_value.c:52: Warning:
Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:56: Warning:
+ Ignore call: not well typed
+[instantiate] tests/string/memset_value.c:57: Warning:
+ Ignore call: not well typed
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -32,6 +36,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
@@ -151,27 +156,36 @@ void with_void(void *dest, int value)
return;
}
+void with_incomplete(struct incomplete *dest, int value)
+{
+ struct incomplete *res = memset((void *)dest,value,(unsigned int)10);
+ memset((void *)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)
[kernel] tests/string/memset_value.c:10: Warning:
- dropping duplicate def'n of func chars at tests/string/memset_value.c:10 in favor of that at tests/string/result/memset_value.c:26
+ dropping duplicate def'n of func chars at tests/string/memset_value.c:10 in favor of that at tests/string/result/memset_value.c:27
[kernel] tests/string/memset_value.c:15: Warning:
- dropping duplicate def'n of func uchars at tests/string/memset_value.c:15 in favor of that at tests/string/result/memset_value.c:50
+ dropping duplicate def'n of func uchars at tests/string/memset_value.c:15 in favor of that at tests/string/result/memset_value.c:51
[kernel] tests/string/memset_value.c:20: Warning:
- dropping duplicate def'n of func nested_chars at tests/string/memset_value.c:20 in favor of that at tests/string/result/memset_value.c:78
+ dropping duplicate def'n of func nested_chars at tests/string/memset_value.c:20 in favor of that at tests/string/result/memset_value.c:79
[kernel] tests/string/memset_value.c:25: Warning:
- dropping duplicate def'n of func integer at tests/string/memset_value.c:25 in favor of that at tests/string/result/memset_value.c:85
+ dropping duplicate def'n of func integer at tests/string/memset_value.c:25 in favor of that at tests/string/result/memset_value.c:86
[kernel] tests/string/memset_value.c:30: Warning:
- dropping duplicate def'n of func with_named at tests/string/memset_value.c:30 in favor of that at tests/string/result/memset_value.c:92
+ dropping duplicate def'n of func with_named at tests/string/memset_value.c:30 in favor of that at tests/string/result/memset_value.c:93
[kernel] tests/string/memset_value.c:35: Warning:
- dropping duplicate def'n of func structure at tests/string/memset_value.c:35 in favor of that at tests/string/result/memset_value.c:99
+ dropping duplicate def'n of func structure at tests/string/memset_value.c:35 in favor of that at tests/string/result/memset_value.c:100
[kernel] tests/string/memset_value.c:40: Warning:
- 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
+ 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:108
[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
+ 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:115
[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
+ 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:123
+[kernel] tests/string/memset_value.c:55: Warning:
+ dropping duplicate def'n of func with_incomplete at tests/string/memset_value.c:55 in favor of that at tests/string/result/memset_value.c:130
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -181,6 +195,7 @@ struct X {
int y ;
};
typedef int named;
+struct incomplete;
/*@ requires in_bounds_value: -128 ≤ value < 128;
requires valid_dest: \valid(ptr + (0 .. len - 1));
ensures
@@ -305,4 +320,11 @@ void with_void(void *dest, int value)
return;
}
+void with_incomplete(struct incomplete *dest, int value)
+{
+ struct incomplete *res = memset((void *)dest,value,(unsigned int)10);
+ memset((void *)res,value,(unsigned int)10);
+ return;
+}
+
--
GitLab