[wp] fix wrong layout for opaque structures

src/plugins/wp/MemTyped.ml

@@ -770,7 +770,7 @@ struct
   let clayout (c: Cil_types.compinfo) : layout =
     match c.cfields with
     | None ->
-        rlayout [] (C_comp c)
+        [Garbled]
     | Some fields ->
         let flayout w f = rlayout w (Ctypes.object_of f.ftype) in
         List.fold_left flayout [] (List.rev fields)

src/plugins/wp/tests/wp_acsl/garbled_opaque_struct.i

+char * f(void);
+void g(void) {
+  struct capture* b = f();
+  //@ assert \valid(b);
+}

src/plugins/wp/tests/wp_acsl/oracle/garbled_opaque_struct.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/garbled_opaque_struct.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] tests/wp_acsl/garbled_opaque_struct.i:2: Warning: 
+  Neither code nor specification for function f, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/garbled_opaque_struct.i:3: Warning: 
+  Cast with incompatible pointers types (source: sint8*) (target: capture*)
+------------------------------------------------------------
+  Function g
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_acsl/garbled_opaque_struct.i, line 4):
+tests/wp_acsl/garbled_opaque_struct.i:3: warning from Typed Model:
+ - Warning: Hide \result
+   Reason: Cast with incompatible pointers types (source: sint8*) (target: capture*)
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_rw(Malloc_0, b, Length_of_S1_capture).
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/garbled_opaque_struct.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/garbled_opaque_struct.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel:annot:missing-spec] tests/wp_acsl/garbled_opaque_struct.i:2: Warning: 
+  Neither code nor specification for function f, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/garbled_opaque_struct.i:3: Warning: 
+  Cast with incompatible pointers types (source: sint8*) (target: capture*)
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo] Goal typed_g_assert : Unsuccess (Stronger)
+[wp] Proved goals:    0 / 1
+  Alt-Ergo:        0  (unsuccess: 1)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  g                         -        -        1       0.0%
+------------------------------------------------------------