From c2bc7ca5b72e13fa1071d9befd8f521e9339ab2d Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 14 Feb 2020 14:39:10 +0100
Subject: [PATCH] [kernel] Revise const folding of const globals.
---
src/kernel_services/ast_queries/cil.ml | 27 ++++---------------
tests/constant_propagation/const_globals.c | 4 ++-
.../oracle/const_globals.res.oracle | 3 ++-
3 files changed, 10 insertions(+), 24 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index b89f97ad217..d19c4462c5a 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 cc4143f5370..41d302fc910 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 d8933a2d754..677f2c3c93b 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; */ ;
--
GitLab