From ec19fdd85f5ff7a0310a35234ae72a6c8a165e94 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 24 Aug 2022 17:56:03 +0200
Subject: [PATCH] [kernel] Fixes Ast_info.possible_value_of_integral_expr

The name seems to imply that it will return Some for any constant integer expression,
not only for integer literals
---
 src/kernel_services/ast_queries/ast_info.ml   |  2 +-
 tests/misc/local_array_non_literal_size.i     | 25 +++++++++++++++++++
 .../local_array_non_literal_size.err.oracle   |  0
 .../local_array_non_literal_size.res.oracle   |  0
 4 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 tests/misc/local_array_non_literal_size.i
 create mode 100644 tests/misc/oracle/local_array_non_literal_size.err.oracle
 create mode 100644 tests/misc/oracle/local_array_non_literal_size.res.oracle

diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index e0e40434a36..52c110ee0e5 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -39,7 +39,7 @@ let rec possible_value_of_integral_const = function
   | _ -> None
 
 and possible_value_of_integral_expr e =
-  match e.enode with
+  match (Cil.constFold true e).enode with
   | Const c -> possible_value_of_integral_const c
   | _ -> None
 
diff --git a/tests/misc/local_array_non_literal_size.i b/tests/misc/local_array_non_literal_size.i
new file mode 100644
index 00000000000..cc8c1cf75ba
--- /dev/null
+++ b/tests/misc/local_array_non_literal_size.i
@@ -0,0 +1,25 @@
+/* run.config
+   PLUGIN: eva,inout
+   OPT: -eva -machdep gcc_x86_64
+*/
+
+void one_dim() {
+  int empty_array[3%1] = { };
+  int normal_array[3+1] = { 0, 1, 2, 3 };
+}
+
+void two_dim_literal() {
+  int empty_array[1][0] = { };
+  int normal_array[1][4] = { 0, 1, 2, 3 };
+}
+
+void two_dim_non_literal () {
+  int empty_array[1][3%1] = { };
+  int normal_array[1][3+1] = { 0, 1, 2, 3 };
+}
+
+int main() {
+  one_dim();
+  two_dim_literal();
+  two_dim_non_literal();
+}
diff --git a/tests/misc/oracle/local_array_non_literal_size.err.oracle b/tests/misc/oracle/local_array_non_literal_size.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/misc/oracle/local_array_non_literal_size.res.oracle b/tests/misc/oracle/local_array_non_literal_size.res.oracle
new file mode 100644
index 00000000000..e69de29bb2d
-- 
GitLab