diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index 2de503910f92d466c89b6d93f5c578c886090c12..90833a758887b71dfbdc755db081e559cd358d98 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 7eb38c401b614467933f6878f9acd748b6f8b847..70f9f1ddac64085bb1eb6af9d121daf21bfe4c85 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 9b0dddba526690da19d148e67a7b72b0269f32cb..c402c3de32d94555743b43391bad9d98ada35d83 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