From ee66f23f3f18ff6d27586099c689e1dcddf5c37d Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 27 Jul 2018 14:03:33 +0200
Subject: [PATCH] [Kernel] remove dead code from rmtmps; minor simplifications
---
src/kernel_internals/typing/rmtmps.ml | 24 ++++++++++++------------
src/kernel_internals/typing/rmtmps.mli | 1 -
src/kernel_services/ast_queries/file.ml | 2 +-
3 files changed, 13 insertions(+), 14 deletions(-)
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 2cc4c84b91a..c1c2fef79e6 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -48,8 +48,10 @@ open Cil_types
open Cil
module H = Hashtbl
-(* Set on the command-line: *)
+(* Used by external plug-ins: *)
let keepUnused = ref false
+
+(* Possibly no longer used: *)
let rmUnusedInlines = ref false
let rmUnusedStatic = ref false
@@ -760,9 +762,7 @@ let removeUnmarked isRoot file =
type rootsFilter = global -> bool
-let isDefaultRoot = isExportedRoot
-
-let removeUnusedTemps ?(isRoot : rootsFilter = isDefaultRoot) file =
+let removeUnusedTemps ?(isRoot : rootsFilter = isExportedRoot) file =
if not !keepUnused then
begin
Kernel.debug ~dkey "Removing unused temporaries" ;
@@ -772,8 +772,8 @@ let removeUnusedTemps ?(isRoot : rootsFilter = isDefaultRoot) file =
(* build up the root set *)
let isRoot global =
- isPragmaRoot keepers global ||
- isRoot global
+ isPragmaRoot keepers global ||
+ isRoot global
in
(* mark everything reachable from the global roots *)
@@ -785,12 +785,12 @@ let removeUnusedTemps ?(isRoot : rootsFilter = isDefaultRoot) file =
(* print which original source variables were removed *)
if false && removedLocals != [] then
- let count = List.length removedLocals in
- if count > 2000 then
- (Kernel.warning "%d unused local variables removed" count)
- else
- (Kernel.warning "%d unused local variables removed:@!%a"
- count (Pretty_utils.pp_list ~sep:",@," Format.pp_print_string) removedLocals)
+ let count = List.length removedLocals in
+ if count > 2000 then
+ (Kernel.warning "%d unused local variables removed" count)
+ else
+ (Kernel.warning "%d unused local variables removed:@!%a"
+ count (Pretty_utils.pp_list ~sep:",@," Format.pp_print_string) removedLocals)
end
(*
diff --git a/src/kernel_internals/typing/rmtmps.mli b/src/kernel_internals/typing/rmtmps.mli
index c99591522f1..61f49635423 100644
--- a/src/kernel_internals/typing/rmtmps.mli
+++ b/src/kernel_internals/typing/rmtmps.mli
@@ -76,7 +76,6 @@
type rootsFilter = Cil_types.global -> bool
-val isDefaultRoot : rootsFilter
val isExportedRoot : rootsFilter
val isCompleteProgramRoot : rootsFilter
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 3e49d89eeee..1f1726189a0 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -637,7 +637,7 @@ let () =
keep_unused_specified_function). This function is meant to be passed to
{!Rmtmps.removeUnusedTemps}. *)
let keep_entry_point ?(specs=Kernel.Keep_unused_specified_functions.get ()) g =
- Rmtmps.isDefaultRoot g ||
+ Rmtmps.isExportedRoot g ||
match g with
| GFun({svar = v; sspec = spec},_)
| GFunDecl(spec,v,_) ->
--
GitLab