From 7921c6448e0f864c9f5b7d0bc3f3e7c7d63d405b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 15 Mar 2022 14:27:40 +0100
Subject: [PATCH] [wp] Fix crash with too large array in MemTyped
---
src/plugins/wp/MemTyped.ml | 4 ++--
.../wp_typed/oracle/too_large_array.0.res.oracle | 11 +++++++++++
.../wp_typed/oracle/too_large_array.1.res.oracle | 11 +++++++++++
src/plugins/wp/tests/wp_typed/too_large_array.i | 15 +++++++++++++++
4 files changed, 39 insertions(+), 2 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_typed/oracle/too_large_array.0.res.oracle
create mode 100644 src/plugins/wp/tests/wp_typed/oracle/too_large_array.1.res.oracle
create mode 100644 src/plugins/wp/tests/wp_typed/too_large_array.i
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 0bee9720d06..49afd0daf84 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -555,8 +555,8 @@ module BASE = WpContext.Generator(Varinfo)
Warning.handle
~handler:(fun _ -> None)
~effect:(Printf.sprintf "No allocation size for variable '%s'" x.vname)
- (fun obj -> Some (length_of_object obj))
- (Ctypes.object_of x.vtype)
+ (fun t -> Some (length_of_object @@ Ctypes.object_of t))
+ x.vtype
let linked prefix x base =
let name = prefix ^ "_linked" in
diff --git a/src/plugins/wp/tests/wp_typed/oracle/too_large_array.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/too_large_array.0.res.oracle
new file mode 100644
index 00000000000..781a8320d60
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle/too_large_array.0.res.oracle
@@ -0,0 +1,11 @@
+# frama-c -wp [...]
+[kernel] Parsing too_large_array.i (no preprocessing)
+[kernel] too_large_array.i:12: Warning:
+ Cannot represent length of array as an attribute
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] too_large_array.i:13: Warning: Array size too large (0xFFFFFFFFFFFFFFFF)
+[wp] too_large_array.i:14: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+[wp] too_large_array.i:11: User Error: Array size too large (0xFFFFFFFFFFFFFFFF)
+[kernel] Plug-in wp aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_typed/oracle/too_large_array.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/too_large_array.1.res.oracle
new file mode 100644
index 00000000000..6242084d18f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle/too_large_array.1.res.oracle
@@ -0,0 +1,11 @@
+# frama-c -wp -wp-model 'Typed (Ref)' [...]
+[kernel] Parsing too_large_array.i (no preprocessing)
+[kernel] too_large_array.i:12: Warning:
+ Cannot represent length of array as an attribute
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] too_large_array.i:13: Warning: Array size too large (0xFFFFFFFFFFFFFFFF)
+[wp] too_large_array.i:14: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+[wp] too_large_array.i:11: User Error: Array size too large (0xFFFFFFFFFFFFFFFF)
+[kernel] Plug-in wp aborted: invalid user input.
diff --git a/src/plugins/wp/tests/wp_typed/too_large_array.i b/src/plugins/wp/tests/wp_typed/too_large_array.i
new file mode 100644
index 00000000000..e545f1f7413
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/too_large_array.i
@@ -0,0 +1,15 @@
+/* run.config
+ EXIT: 1
+ STDOPT:
+*/
+/* run.config_qualif
+ DONTRUN:
+*/
+
+/*@ predicate P{L}(int* a) = *a == 42 ; */
+
+void merge(void) {
+ int tmp[0xFFFFFFFFFFFFFFFFULL];
+ //@ loop invariant sorted: P(&tmp[0]);
+ while(1){}
+}
--
GitLab