diff --git a/Makefile b/Makefile
index 5136dd9a8b93c557310c9baea7309210b55371ed..d72ead1c599395731de6ce68dd59559fbe4a8410 100644
--- a/Makefile
+++ b/Makefile
@@ -565,6 +565,7 @@ KERNEL_CMO=\
src/kernel_internals/typing/rmtmps.cmo \
src/kernel_internals/typing/oneret.cmo \
src/kernel_internals/typing/frontc.cmo \
+ src/kernel_internals/typing/substitute_const_globals.cmo \
src/kernel_services/analysis/ordered_stmt.cmo \
src/kernel_services/analysis/wto_statement.cmo \
src/kernel_services/analysis/dataflows.cmo \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index f93a3797c6f1586aaeaa52de9858856bd5509e5b..035be22244998a83b6c849bbf177f4298364856e 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -405,6 +405,8 @@ src/kernel_internals/typing/translate_lightweight.ml: CEA_INRIA_LGPL
src/kernel_internals/typing/translate_lightweight.mli: CEA_INRIA_LGPL
src/kernel_internals/typing/unroll_loops.ml: CEA_LGPL
src/kernel_internals/typing/unroll_loops.mli: CEA_LGPL
+src/kernel_internals/typing/substitute_const_globals.ml: CEA_LGPL
+src/kernel_internals/typing/substitute_const_globals.mli: CEA_LGPL
src/kernel_services/README.md: .ignore
src/kernel_services/abstract_interp/README.md: .ignore
src/kernel_services/abstract_interp/abstract_interp.ml: CEA_LGPL
diff --git a/src/kernel_internals/typing/substitute_const_globals.ml b/src/kernel_internals/typing/substitute_const_globals.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f83359c0980171c11e5bd7e8d37a716598389574
--- /dev/null
+++ b/src/kernel_internals/typing/substitute_const_globals.ml
@@ -0,0 +1,109 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* Syntactic substitution of globals, defined with the attribute 'const', with
+ respective initializers. *)
+
+open Cil_types
+open Cil_datatype
+open Cil
+
+class constGlobSubstVisitorClass : cilVisitor = object
+ inherit nopCilVisitor
+
+ val vi_to_init_opt = Varinfo.Hashtbl.create 7
+
+ (* Visit globals and register only the association between globals with attribute
+ 'const' and respective initializers. *)
+ method! vglob g =
+ let rec is_arithmetic_type = function
+ | TArray (typ, _, _, _) -> is_arithmetic_type typ
+ | TInt _ | TFloat _ | TEnum _ -> true
+ | _ -> false
+ in
+ match g with
+ | GVar (vi, _, _) ->
+ (* Register in [vi_to_init_opt] the association between [vi] and its
+ 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
+ pattern matching. *)
+ assert false
+ in
+ let typ = unrollTypeDeep vi.vtype in
+ if is_arithmetic_type typ && isConstType typ
+ then ChangeDoChildrenPost ([g], List.map register)
+ else DoChildren
+ | _ ->
+ DoChildren
+
+ (* Visit expressions and replace lvals, with a registered varinfo in
+ [vi_to_init_opt], with respective initializing constant expressions. *)
+ method! vexpr e =
+ match e.enode with
+ | Lval (Var vi, (NoOffset | Index _ as offset)) ->
+ (* Support for variables and array, on arithmetic types only. *)
+ begin match Varinfo.Hashtbl.find vi_to_init_opt vi with
+ | None ->
+ (* Since [vi] is a global, we replace it with the zero expression,
+ i.e. the implicit initializer for such globals. *)
+ let newexp = zero ~loc:e.eloc in
+ ChangeTo newexp
+ | Some init ->
+ let offset = constFoldOffset true offset in
+ let zero_exp = zero ~loc:e.eloc in
+ let rec find_replace current_offset current_init current_newexp =
+ match current_init with
+ | SingleInit si ->
+ if Cil_datatype.OffsetStructEq.equal offset current_offset
+ then new_exp ~loc:e.eloc si.enode
+ else current_newexp
+ | CompoundInit (ct, initl) ->
+ (* We are dealing with an array: recursively [find_replace] among
+ its initializers. *)
+ foldLeftCompound
+ ~implicit:true
+ ~doinit:(fun coffset cinit _ acc ->
+ find_replace
+ (addOffset coffset current_offset)
+ cinit
+ acc)
+ ~ct
+ ~initl
+ ~acc:current_newexp
+ in
+ let newexp = find_replace NoOffset init zero_exp in
+ ChangeTo newexp
+ | exception Not_found ->
+ DoChildren
+ end
+ | _ ->
+ DoChildren
+end
+
+let constGlobSubstVisitor = new constGlobSubstVisitorClass
diff --git a/src/kernel_internals/typing/substitute_const_globals.mli b/src/kernel_internals/typing/substitute_const_globals.mli
new file mode 100644
index 0000000000000000000000000000000000000000..b38eba1ea90bd212460e9f2cbb6db5b95e17ebb7
--- /dev/null
+++ b/src/kernel_internals/typing/substitute_const_globals.mli
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** A visitor that substitutes globals, defined with the attribute 'const', with
+ respective initializers. *)
+val constGlobSubstVisitor: Cil.cilVisitor
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index d19c4462c5a0b2174ee065e11726de1e97b85011..296fe6418d175111fe618bb268b5ba7319a131c5 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6305,86 +6305,6 @@ let foldLeftCompound
| _ -> Kernel.fatal ~current:true "Type of Compound is not array or struct or union"
-class constGlobSubstVisitorClass : cilVisitor = object
- inherit nopCilVisitor
-
- val vi_to_init_opt = Varinfo.Hashtbl.create 7
-
- (* Visit globals and register only the association between globals with attribute
- 'const' and respective initializers. *)
- method! vglob g =
- let rec is_arithmetic_type = function
- | TArray (typ, _, _, _) -> is_arithmetic_type typ
- | TInt _ | TFloat _ | TEnum _ -> true
- | _ -> false
- in
- match g with
- | GVar (vi, _, _) ->
- (* Register in [vi_to_init_opt] the association between [vi] and its
- 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
- pattern matching. *)
- assert false
- in
- let typ = unrollTypeDeep vi.vtype in
- if is_arithmetic_type typ && isConstType typ
- then ChangeDoChildrenPost ([g], List.map register)
- else DoChildren
- | _ ->
- DoChildren
-
- (* Visit expressions and replace lvals, with a registered varinfo in
- [vi_to_init_opt], with respective initializing constant expressions. *)
- method! vexpr e =
- match e.enode with
- | Lval (Var vi, (NoOffset | Index _ as offset)) ->
- (* Support for variables and array, on arithmetic types only. *)
- begin match Varinfo.Hashtbl.find vi_to_init_opt vi with
- | None ->
- (* Since [vi] is a global, we replace it with the zero expression,
- i.e. the implicit initializer for such globals. *)
- let newexp = zero ~loc:e.eloc in
- ChangeTo newexp
- | Some init ->
- let offset = constFoldOffset true offset in
- let zero_exp = zero ~loc:e.eloc in
- let rec find_replace current_offset current_init current_newexp =
- match current_init with
- | SingleInit si ->
- if Cil_datatype.OffsetStructEq.equal offset current_offset
- then new_exp ~loc:e.eloc si.enode
- else current_newexp
- | CompoundInit (ct, initl) ->
- (* We are dealing with an array: recursively [find_replace] among
- its initializers. *)
- foldLeftCompound
- ~implicit:true
- ~doinit:(fun coffset cinit _ acc ->
- find_replace
- (addOffset coffset current_offset)
- cinit
- acc)
- ~ct
- ~initl
- ~acc:current_newexp
- in
- let newexp = find_replace NoOffset init zero_exp in
- ChangeTo newexp
- | exception Not_found ->
- DoChildren
- end
- | _ ->
- DoChildren
-end
-let constGlobSubstVisitor = new constGlobSubstVisitorClass
-
let has_flexible_array_member t =
let is_flexible_array t =
match unrollType t with
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index c04e0fb5423ba56e143c6533bfadc59955436680..564979fc95ae2a5017bdb73ecb1e062a7dfb3901 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -893,6 +893,10 @@ val constFoldTermNodeAtTop: term_node -> term_node
and [alignof]. *)
val constFoldTerm: bool -> term -> term
+(** Do constant folding on a {!Cil_types.offset}. If the second argument is true
+ then will also compute compiler-dependent expressions such as [sizeof]. *)
+val constFoldOffset: bool -> offset -> offset
+
(** Do constant folding on a binary operation. The bulk of the work done by
[constFold] is done here. If the second argument is true then
will also compute compiler-dependent expressions such as [sizeof]. *)
@@ -1971,10 +1975,6 @@ val is_skip: stmtkind -> bool
machine specific simplifications to be done, or not. *)
val constFoldVisitor: bool -> cilVisitor
-(** A visitor that substitutes globals, defined with the attribute 'const', by
- their constant initializing expressions. *)
-val constGlobSubstVisitor: cilVisitor
-
(* ************************************************************************* *)
(** {2 Debugging support} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 0737eb2419b220bd49f03d39e37e97f8fb6d2117..32b6ac62cbad411e1f4e2095cf0ce970a35c6225 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -1105,7 +1105,10 @@ let () =
let constglobfold = register_code_transformation_category "constglobfold" in
let syntactic_const_globals_substitution ast =
if Kernel.Constfold.get ()
- then Cil.visitCilFileSameGlobals Cil.constGlobSubstVisitor ast
+ then
+ Cil.visitCilFileSameGlobals
+ Substitute_const_globals.constGlobSubstVisitor
+ ast
in
add_code_transformation_before_cleanup
~deps:[ (module Kernel.Constfold: Parameter_sig.S) ]