From cdba1f48ede4afca87cee449bca566e625a96fac Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 25 Mar 2020 17:48:39 +0100
Subject: [PATCH] [Instantiate] Memset: take of nested typedefs

---
 src/plugins/instantiate/string/memset.ml      |  2 +-
 .../tests/string/memset_nested_typedef.c      |  9 +++
 .../oracle/memset_nested_typedef.res.oracle   | 75 +++++++++++++++++++
 3 files changed, 85 insertions(+), 1 deletion(-)
 create mode 100644 src/plugins/instantiate/tests/string/memset_nested_typedef.c
 create mode 100644 src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle

diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml
index f1935a41528..7c2bc6ce40c 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 00000000000..2e01be12e5c
--- /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 00000000000..27287ebadeb
--- /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;
+}
+
+
-- 
GitLab