diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml index f1935a41528667bcf05f6313dd1e226bf04b5279..7c2bc6ce40cf17a3d39c2456e54e319d5685ec11 100644 --- a/src/plugins/instantiate/string/memset.ml +++ b/src/plugins/instantiate/string/memset.ml @@ -63,7 +63,7 @@ let pset_len_bytes_to_value ?loc ptr value bytes_len = let pset_len_bytes_to_zero ?loc ptr bytes_len = let eq_value ?loc t = - let value = match t.term_type with + let value = match Logic_utils.unroll_type t.term_type with | Ctype(TPtr(_)) -> term Tnull t.term_type | Ctype(TFloat(_)) -> treal ?loc 0. | Ctype(TInt(_)) -> tinteger ?loc 0 diff --git a/src/plugins/instantiate/tests/string/memset_nested_typedef.c b/src/plugins/instantiate/tests/string/memset_nested_typedef.c new file mode 100644 index 0000000000000000000000000000000000000000..2e01be12e5c6560ef86b35bbcd997ead76b61e00 --- /dev/null +++ b/src/plugins/instantiate/tests/string/memset_nested_typedef.c @@ -0,0 +1,9 @@ +#include <string.h> + +typedef unsigned t; +struct X { t s_addr; }; + +void test() { + struct X x; + memset(&x, 0, sizeof(x)); +} diff --git a/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..27287ebadeb96af03f306779f2dcf0043d0fbf8d --- /dev/null +++ b/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle @@ -0,0 +1,75 @@ +[kernel] Parsing tests/string/memset_nested_typedef.c (with preprocessing) +/* Generated by Frama-C */ +#include "stddef.h" +#include "string.h" +#include "strings.h" +typedef unsigned int t; +struct X { + t s_addr ; +}; +/*@ requires aligned_end: len % 4 ≡ 0; + requires + valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1)); + ensures + set_content: + \let __fc_len = len / 4; + ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ (ptr + j0)->s_addr ≡ 0; + ensures result: \result ≡ ptr; + assigns *(ptr + (0 .. len / 4 - 1)), \result; + assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing; + assigns \result \from ptr; + */ +struct X *memset_st_X_0(struct X *ptr, size_t len) +{ + struct X *__retres; + __retres = (struct X *)memset((void *)ptr,0,len); + return __retres; +} + +void test(void) +{ + struct X x; + memset_st_X_0(& x,sizeof(x)); + return; +} + + +[kernel] Parsing tests/string/result/memset_nested_typedef.c (with preprocessing) +[kernel] Parsing tests/string/memset_nested_typedef.c (with preprocessing) +[kernel] tests/string/memset_nested_typedef.c:6: Warning: + dropping duplicate def'n of func test at tests/string/memset_nested_typedef.c:6 in favor of that at tests/string/result/memset_nested_typedef.c:28 +/* Generated by Frama-C */ +#include "stddef.h" +#include "string.h" +#include "strings.h" +typedef unsigned int t; +struct X { + t s_addr ; +}; +/*@ requires aligned_end: len % 4 ≡ 0; + requires + valid_dest: \let __fc_len = len / 4; \valid(ptr + (0 .. __fc_len - 1)); + ensures + set_content: + \let __fc_len = \old(len) / 4; + ∀ ℤ j0; 0 ≤ j0 < __fc_len ⇒ (\old(ptr) + j0)->s_addr ≡ 0; + ensures result: \result ≡ \old(ptr); + assigns *(ptr + (0 .. len / 4 - 1)), \result; + assigns *(ptr + (0 .. len / 4 - 1)) \from \nothing; + assigns \result \from ptr; + */ +struct X *memset_st_X_0(struct X *ptr, size_t len) +{ + struct X *__retres; + __retres = (struct X *)memset((void *)ptr,0,len); + return __retres; +} + +void test(void) +{ + struct X x; + memset_st_X_0(& x,sizeof(x)); + return; +} + +