diff --git a/src/plugins/instantiate/string/memcmp.ml b/src/plugins/instantiate/string/memcmp.ml
index 813ab06065ffd8950c70eee109e2c9f264d69a64..e493cbb3939b7e39c998d5554343adacd938e429 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 6be6f6664ba02549639d9674ce51f19f7875e8a2..02d06b3d5ea985304f4dcac455ddd142220211a2 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 97c3dcb1c577525df2f2caccc210a574cf54a81c..75aef926971ae0b428b462ccccbb47b5682ff361 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 d597bd3a452b3eeeb7d57e3d5bd8bc361500033e..79c0fd60bbe890272f8e4c7d15e0dae5148d0321 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 004f004f222223440c8a3221832d494ecd8541ce..404692f9eb118b24ffa7716dceb72b990d973d2e 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 4f245bbbd068b03d854f4dbf7571693be07af82f..f2c6c03d864470e963082de31044b103dde3a930 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 9fca890b0e18cd35a23f399ee9bf2d86262e6e65..a40698297fd597433f1ced51585f2c1176b285f7 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 25f04a59ff02c4378a30f44a82d1ffa81758f895..432b8ed6a6d3aa03bbb2d99e449641a6e4ac7d1c 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 9a3d0e6381121a41265d270e492b2b5ffca83dc7..9d73f30f20f905d89a6c876dc03d7073fea77b64 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 63bd23cf23c207e89a094717492cd87246acb3c0..a9bc6101a2559efcdea518a23edee96a2c15b8ce 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 6023a30c6bf1db32b311e1cc205aa6780273e26c..9d8a290eff81051c3604270ef849c034f8a06be7 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 26ed27864cc376fc2578df1e457c44cec81850ec..e0a760dc1f0cab9e4c804ab2062afab1466f796a 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;
+}
+