diff options
-rw-r--r-- | cparser/Parse.ml | 2 | ||||
-rw-r--r-- | cparser/Rename.ml | 29 | ||||
-rw-r--r-- | cparser/Rename.mli | 2 | ||||
-rw-r--r-- | driver/Clflags.ml | 1 | ||||
-rw-r--r-- | driver/Driver.ml | 8 | ||||
-rw-r--r-- | driver/Optionsprinter.ml | 1 |
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 |