diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml index 2cc4c84b91adf8d54d4ffb42b36ce889c651aa7c..c1c2fef79e6ce2c0982503ace7367d26cf32742c 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 c99591522f1790b69002d4ed3a572c01067441dd..61f496354236aac967e2bd4862dc037fd4248b72 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 3e49d89eeee42a19df6936e96e16b390e18ba209..1f1726189a09cf9422cab0e6a3d1c11e3c29f5cf 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,_) ->