diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index b89f97ad2171eccfff406f8e602320e2c9b13a73..d19c4462c5a0b2174ee065e11726de1e97b85011 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -6318,40 +6318,23 @@ class constGlobSubstVisitorClass : cilVisitor = object | TInt _ | TFloat _ | TEnum _ -> true | _ -> false in - let has_attribute_const typ = - let rec typeAttr = function - | TArray (typ, _, _, _) -> - typeAttr typ - | TVoid a - | TInt (_, a) - | TFloat (_, a) - | TNamed (_, a) - | TPtr (_, a) - | TComp (_, _, a) - | TEnum (_, a) - | TFun (_, _, _, a) - | TBuiltin_va_list a -> - a - in - hasAttribute "const" (typeAttr typ) - in match g with | GVar (vi, _, _) -> (* Register in [vi_to_init_opt] the association between [vi] and its - initializer [init_opt]. The is assumed to be an expression of literal - constants only, as the lvals originally appearing in it have been - substituted by the respective initializers in [vexpr]. *) + initializer [init_opt]. The latter is assumed to be an expression of + literal constants only, as the lvals originally appearing in it have + been substituted by the respective initializers in method [vexpr]. *) let register = function | GVar (vi, { init = init_opt }, _loc) as g -> Varinfo.Hashtbl.add vi_to_init_opt vi init_opt; g | _ -> (* Cannot happen as we treat only [GVar _] cases in the outer - patter matching. *) + pattern matching. *) assert false in let typ = unrollTypeDeep vi.vtype in - if is_arithmetic_type typ && has_attribute_const typ + if is_arithmetic_type typ && isConstType typ then ChangeDoChildrenPost ([g], List.map register) else DoChildren | _ -> diff --git a/tests/constant_propagation/const_globals.c b/tests/constant_propagation/const_globals.c index cc4143f5370a5b2914eed5ff2ef258168f580a25..41d302fc9106813b0a3da4c52b48ffac1de18349 100644 --- a/tests/constant_propagation/const_globals.c +++ b/tests/constant_propagation/const_globals.c @@ -4,7 +4,9 @@ #include <stddef.h> -static const size_t c1 = 300; +typedef const size_t const_size_t; + +static const_size_t c1 = 300; static const size_t c2[2] = { 5, c1 + 1 + c1 }; static const size_t c3[3][2][4] = { [0][0][0] = c2[0], diff --git a/tests/constant_propagation/oracle/const_globals.res.oracle b/tests/constant_propagation/oracle/const_globals.res.oracle index d8933a2d754fa00b65a8c8cba355c4576422226d..677f2c3c93b361eaf104cc5be2e6cc6e0f9053bc 100644 --- a/tests/constant_propagation/oracle/const_globals.res.oracle +++ b/tests/constant_propagation/oracle/const_globals.res.oracle @@ -1,7 +1,8 @@ [kernel] Parsing tests/constant_propagation/const_globals.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" -static size_t const c1 = 300U; +typedef size_t const const_size_t; +static const_size_t c1 = 300U; size_t f(size_t y) { /*@ assert c1 ≡ 300; */ ;