diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml index 0bee9720d0670116e6b1f4e2fe5a63f7a0b75d61..49afd0daf8477891d63f6077707ccae5df4d48c5 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 0000000000000000000000000000000000000000..781a8320d6073f068ea7888089a723cea2b710e6 --- /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 0000000000000000000000000000000000000000..6242084d18f6309927ded59be9f34e0b814753a1 --- /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 0000000000000000000000000000000000000000..e545f1f741383217d61c9500b911664aeb248874 --- /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){} +}