diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index b14ad59df17dc996dabd4f936fafaebc2d1bebc5..f3b479e9c0745c243ba404dee8ce6e8acd4e4c8b 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/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") diff --git a/tests/misc/array_size_specifier_unification.i b/tests/misc/array_size_specifier_unification.i new file mode 100644 index 0000000000000000000000000000000000000000..97b90a4a11980ed20830c12168308e6b001aff28 --- /dev/null +++ b/tests/misc/array_size_specifier_unification.i @@ -0,0 +1,15 @@ +/* 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; } diff --git a/tests/misc/oracle/array_size_specifier_unification.res.oracle b/tests/misc/oracle/array_size_specifier_unification.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..67eddb894c94d71be47d2fd7661b2cc97a64d078 --- /dev/null +++ b/tests/misc/oracle/array_size_specifier_unification.res.oracle @@ -0,0 +1,13 @@ +[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; +} + +