|wp] Intercept 0 size arrays when typing

src/plugins/wp/ctypes.ml

@@ -245,6 +245,14 @@ let constant e =
       end
   | _ -> Warning.error "Non-constant expression (%a)" Printer.pp_exp e
 
+let array_size = function
+  | None -> None
+  | Some e ->
+      match constant e with
+      | 0L when Cil.gccMode () || Cil.msvcMode () -> None
+      | 0L -> Warning.error "0 sized array only allowed in GCC/MSVC mode"
+      | n  -> Some n
+
 let get_int e =
   match (Cil.constFold true e).enode with
   | Const(CInt64(k,_,_)) -> Some (Integer.to_int_exn k)
@@ -281,7 +289,7 @@ let rec object_of typ =
   | TComp (comp,_,_) -> C_comp comp
   | TArray (typ_elt,e_opt,_,_) ->
       begin
-        match e_opt with
+        match array_size e_opt with
         | None ->
             C_array {
               arr_element = typ_elt;
@@ -292,7 +300,7 @@ let rec object_of typ =
             C_array {
               arr_element = typ_elt ;
               arr_flat = Some {
-                  arr_size = Int64.to_int (constant e) ;
+                  arr_size = Int64.to_int e ;
                   arr_dim = dim ;
                   arr_cell = ty_cell ;
                   arr_cell_nbr = ncells ;

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

+/* run.config
+   STDOPT: #"-rte -machdep gcc_x86_32"
+*/
+/* run.config_qualif
+   STDOPT: #"-rte -machdep gcc_x86_32"
+*/
+
+/*@ assigns \result; */
+void *alloc(void);
+
+struct S { int fam[0]; };
+
+int main (void) {
+	struct S* s = alloc();
+  return s->fam[0];
+}

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

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/gnu_zero_array.i (no preprocessing)
+[rte] annotating function main
+[wp] Running WP plugin...
+[wp] tests/wp_acsl/gnu_zero_array.i:14: Warning: 
+  Cast with incompatible pointers types (source: sint8*) (target: S*)
+------------------------------------------------------------
+  Function main
+------------------------------------------------------------
+
+Goal Assertion 'rte,mem_access' (file tests/wp_acsl/gnu_zero_array.i, line 15):
+tests/wp_acsl/gnu_zero_array.i:14: warning from Typed Model:
+ - Warning: Hide \result
+   Reason: Cast with incompatible pointers types (source: sint8*) (target: S*)
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_rd(Malloc_0, shift_sint32(shiftfield_F1_S_fam(s), 0), 1).
+
+------------------------------------------------------------

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

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/gnu_zero_array.i (no preprocessing)
+[rte] annotating function main
+[wp] Running WP plugin...
+[wp] tests/wp_acsl/gnu_zero_array.i:14: Warning: 
+  Cast with incompatible pointers types (source: sint8*) (target: S*)
+[wp] 1 goal scheduled
+[wp] [Alt-Ergo] Goal typed_main_assert_rte_mem_access : Unsuccess (Stronger)
+[wp] Proved goals:    0 / 1
+  Alt-Ergo:        0  (unsuccess: 1)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  main                      -        -        1       0.0%
+------------------------------------------------------------