From 24c02301a53bb88be04c8e95ca3fb521cd6a5d17 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 5 Jul 2024 19:01:18 +0200
Subject: [PATCH] [typing] fix isConstant test for global initialization
---
src/kernel_services/ast_queries/cil.ml | 10 ++++++----
tests/syntax/ko_global.c | 2 +-
tests/syntax/oracle/ko_global.res.oracle | 2 ++
3 files changed, 9 insertions(+), 5 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 2de503910f9..90833a75888 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5881,10 +5881,12 @@ let rec isConstantGen lit_only is_varinfo_cst f e = match e.enode with
begin
match t, typeOf e with
| TInt (i, _), TPtr _ ->
- (* gcc/clang/ccomp consider a non-truncated pointer to be a constant.
- If it is truncated, we check whether we already know its value. *)
- bytesSizeOfInt theMachine.upointKind <= bytesSizeOfInt i ||
- isConstantGen true is_varinfo_cst f e
+ (* gcc/clang/ccomp only consider non-truncated constant ptr values
+ to be constant. If it is truncated, we consider it non-const
+ in any case.
+ *)
+ bytesSizeOfInt theMachine.upointKind <= bytesSizeOfInt i &&
+ isConstantGen false is_varinfo_cst f e
| _ -> isConstantGen lit_only is_varinfo_cst f e
end
| AddrOf (Var vi, off) | StartOf (Var vi, off) ->
diff --git a/tests/syntax/ko_global.c b/tests/syntax/ko_global.c
index 7eb38c401b6..70f9f1ddac6 100644
--- a/tests/syntax/ko_global.c
+++ b/tests/syntax/ko_global.c
@@ -22,7 +22,7 @@ const int f = f;
int g = g;
-int h = (int) &h;
+short h = (short) &h;
const int i;
int j = i;
diff --git a/tests/syntax/oracle/ko_global.res.oracle b/tests/syntax/oracle/ko_global.res.oracle
index 9b0dddba526..c402c3de32d 100644
--- a/tests/syntax/oracle/ko_global.res.oracle
+++ b/tests/syntax/oracle/ko_global.res.oracle
@@ -3,6 +3,8 @@
[kernel] ko_global.c:11: User Error: a is not a compile-time constant
[kernel] ko_global.c:21: User Error: f is not a compile-time constant
[kernel] ko_global.c:23: User Error: g is not a compile-time constant
+[kernel] ko_global.c:25: User Error:
+ Initializer element is not a compile-time constant
[kernel] ko_global.c:28: User Error: i is not a compile-time constant
[kernel] ko_global.c:31: User Error: k is not a compile-time constant
[kernel] ko_global.c:38: User Error: n is not a compile-time constant
--
GitLab