From 8e70660f73babe4f777538f0079a4a00c78a43c4 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 6 Dec 2019 14:42:58 +0100
Subject: [PATCH] Unify array declarations when array size is a same integer
constant value with different type.
---
src/kernel_internals/typing/cabs2cil.ml | 13 ++++++++-----
tests/misc/array_size_specifier_unification.i | 15 +++++++++++++++
.../array_size_specifier_unification.res.oracle | 13 +++++++++++++
3 files changed, 36 insertions(+), 5 deletions(-)
create mode 100644 tests/misc/array_size_specifier_unification.i
create mode 100644 tests/misc/oracle/array_size_specifier_unification.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b14ad59df17..f3b479e9c07 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 00000000000..97b90a4a119
--- /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 00000000000..67eddb894c9
--- /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;
+}
+
+
--
GitLab