Remove undocumented option. Bug 20193

6 files changed, 10 insertions, 33 deletions

diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index 507aea36..dceb9b11 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -24,7 +24,7 @@ let transform_program t p name =
   (run_pass Unblock.program 'b'
   (run_pass Bitfields.program 'f'
   p)))) in
-  (Rename.program p1 (Filename.chop_suffix name ".c"))
+  (Rename.program p1)
 
 let parse_transformations s =
   let t = ref CharSet.empty in
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index c62c6763..c1f31977 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -43,17 +43,6 @@ let enter_public env id =
       re_public = StringMap.add id.name id env.re_public;
       re_used = StringSet.add id.name env.re_used }
 
-let enter_static env id file =
-  try
-    let id' = StringMap.find id.name env.re_public in
-    { env with re_id = IdentMap.add id id' env.re_id }
-  with Not_found ->
-    let file = String.map (fun a -> match a with 'a'..'z' | 'A'..'Z' | '0'..'9' -> a | _ -> '_') file in
-    let id' = {id with name = Printf.sprintf "_%s_%s" file id.name} in
-    { re_id = IdentMap.add id id' env.re_id;
-      re_public = env.re_public;
-      re_used = StringSet.add id'.name env.re_used }
-
 (* For static or local identifiers, we make up a new name if needed *)
 (* If the same identifier has already been declared,
    don't rename a second time *)
@@ -260,7 +249,7 @@ let reserve_builtins () =
 
 (* Reserve global declarations with public visibility *)
 
-let rec reserve_public env file = function
+let rec reserve_public env = function
   | [] -> env
   | dcl :: rem ->
       let env' =
@@ -268,27 +257,21 @@ let rec reserve_public env file = function
         | Gdecl(sto, id, _, _) ->
             begin match sto with
             | Storage_default | Storage_extern -> enter_public env id
-            | Storage_static -> if !Clflags.option_rename_static then
-                enter_static env id file
-                  else
-                env
+            | Storage_static -> env
             | _ -> assert false
             end
         | Gfundef f ->
             begin match f.fd_storage with
             | Storage_default | Storage_extern -> enter_public env f.fd_name
-            | Storage_static -> if !Clflags.option_rename_static then
-                enter_static env f.fd_name file
-            else
-                env
+            | Storage_static -> env
             | _ -> assert false
             end
         | _ -> env in
-      reserve_public env' file rem
+      reserve_public env' rem
 
 (* Rename the program *)
 
-let program p file =
+let program p =
   globdecls
-    (reserve_public (reserve_builtins()) file p)
+    (reserve_public (reserve_builtins()) p)
     [] p
diff --git a/cparser/Rename.mli b/cparser/Rename.mli
index c4ef2228..818a51bc 100644
--- a/cparser/Rename.mli
+++ b/cparser/Rename.mli
@@ -13,4 +13,4 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-val program : C.program -> string -> C.program
+val program : C.program -> C.program
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 6a695aa4..f8c38a54 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -60,6 +60,5 @@ let option_small_data =
        then 8 else 0)
 let option_small_const = ref (!option_small_data)
 let option_timings = ref false
-let option_rename_static = ref false
 let stdlib_path = ref Configuration.stdlib_path
 let use_standard_headers =  ref Configuration.has_standard_headers
diff --git a/driver/Driver.ml b/driver/Driver.ml
index edee32cf..25d80524 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -255,8 +255,6 @@ let version_string =
   else
     "The CompCert C verified compiler, version "^ Version.version ^ "\n"
 
-let gnu_system = Configuration.system <> "diab"
-
 let gnu_debugging_help =
 "  -gdwarf-       Generate debug information in DWARF v2 or DWARF v3\n"
 
@@ -266,8 +264,7 @@ let debugging_help =
 \  -gdepth <n>    Control generation of debugging information\n\
 \                 (<n>=0: none, <n>=1: only-globals, <n>=2: globals + locals\n\
 \                 without locations, <n>=3: full;)\n"
-^ (if gnu_system then gnu_debugging_help else "")^
-"  -frename-static Rename static functions and declarations\n"
+^ (if gnu_system then gnu_debugging_help else "")
 
 let target_help = if Configuration.arch = "arm" then
 "Target processor options:\n\
@@ -408,8 +405,7 @@ let cmdline_actions =
     [ Exact "-gdwarf-2", Unit (dwarf_version 2);
       Exact "-gdwarf-3", Unit (dwarf_version 3);]
   else []) @
- [ Exact "-frename-static", Set option_rename_static;
-   Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin
+ [ Exact "-gdepth", Integer (fun n -> if n = 0 || n <0 then begin
      option_g := false
    end else begin
      option_g := true;
diff --git a/driver/Optionsprinter.ml b/driver/Optionsprinter.ml
index 9dce8592..00b5f5ec 100644
--- a/driver/Optionsprinter.ml
+++ b/driver/Optionsprinter.ml
@@ -64,7 +64,6 @@ let print_clflags oc =
   p_jmember oc "small_data" p_jint !option_small_data;
   p_jmember oc "small_data" p_jint !option_small_const;
   p_jmember oc "timings" p_jbool !option_timings;
-  p_jmember oc "rename_static" p_jbool !option_rename_static;
   fprintf oc "\n}"
 
 let print_struct_passing_style oc = function