Unify array declarations when array size is a same integer constant value with different type.

src/kernel_internals/typing/cabs2cil.ml

@@ -2597,12 +2597,15 @@ let rec combineTypes (what: combineWhat) (oldt: typ) (t: typ) : typ =
       | Some _, None -> oldsz
       | None, None -> sz
       | Some oldsz', Some sz' ->
-        (* They are not structurally equal. But perhaps they are equal if
-         * we evaluate them. Check first machine independent comparison  *)
+        (* They are not structurally equal. But perhaps they are equal if we
+           evaluate them. Check first machine independent comparison. *)
         let checkEqualSize (machdep: bool) =
+          let size_t = Cil.theMachine.Cil.typeOfSizeOf in
+          let size_t_oldsz' = Cil.mkCast ~force:false ~e:oldsz' ~newt:size_t in
+          let size_t_sz' = Cil.mkCast ~force:false ~e:sz' ~newt:size_t in
           ExpStructEq.equal
-            (constFold machdep oldsz')
-            (constFold machdep sz')
+            (constFold machdep size_t_oldsz')
+            (constFold machdep size_t_sz')
         in
         if checkEqualSize false then
           oldsz
@@ -2610,7 +2613,7 @@ let rec combineTypes (what: combineWhat) (oldt: typ) (t: typ) : typ =
           Kernel.warning ~current:true
             "Array type comparison succeeds only based on machine-dependent \
              constant evaluation: %a and %a\n"
-            Cil_printer.pp_exp oldsz' Cil_printer.pp_exp sz' ;
+            Cil_printer.pp_exp oldsz' Cil_printer.pp_exp sz';
           oldsz
         end else
           raise (Cannot_combine "different array lengths")

tests/misc/array_size_specifier_unification.i

+/* run.config
+   OPT: -print -check
+*/
+
+extern int t[3U];
+int t[2+1];
+int t[4/4 + 2];
+
+extern int c[2147483648];
+int c[2147483647+1U];
+
+extern int u[5+5];
+int u[5LL+5];
+
+int main(void){ return 0; }

tests/misc/oracle/array_size_specifier_unification.res.oracle

+[kernel] Parsing tests/misc/array_size_specifier_unification.i (no preprocessing)
+/* Generated by Frama-C */
+int t[3U];
+int c[2147483648];
+int u[5 + 5];
+int main(void)
+{
+  int __retres;
+  __retres = 0;
+  return __retres;
+}
+
+