From a640f7553c653bd3a6cc4fae2bd928638d6751c0 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Fri, 1 Apr 2022 16:29:52 -0700 Subject: [PATCH] New option: -fno-short-names, to retain a prefix on private (static inline) declarations within C files Note that -no-prefix *does* retain precedence over this. This fixes #246 --- src/GlobalNames.ml | 2 +- src/Karamel.ml | 4 ++++ src/Options.ml | 1 + 3 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/GlobalNames.ml b/src/GlobalNames.ml index 78a99c38f..c1d7a7404 100644 --- a/src/GlobalNames.ml +++ b/src/GlobalNames.ml @@ -240,7 +240,7 @@ let target_c_name ~attempt_shortening ~is_macro lid = let pre_name = if skip_prefix lid && not (ineligible lid) then snd lid - else if attempt_shortening && not (ineligible lid) && snd lid <> "main" then + else if attempt_shortening && !Options.short_names && not (ineligible lid) && snd lid <> "main" then snd lid else match rename_prefix lid with | Some prefix -> diff --git a/src/Karamel.ml b/src/Karamel.ml index a994278c7..56d27dec0 100644 --- a/src/Karamel.ml +++ b/src/Karamel.ml @@ -305,6 +305,10 @@ Supported options:|} tweaks"; "-fextern-c", Arg.Set Options.extern_c, " wrap declarations in each header \ with extern \"C\" {"; + "-fnoshort-names", Arg.Clear Options.short_names, " disable unprefix names \ + for private (static) functions that are not exposed in headers; this ensures \ + robust collision-avoidance in case your private function names collide with \ + one of the included system headers"; "", Arg.Unit (fun _ -> ()), " "; (* For developers *) diff --git a/src/Options.ml b/src/Options.ml index bcfbe658b..01991a79a 100644 --- a/src/Options.ml +++ b/src/Options.ml @@ -64,6 +64,7 @@ let merge_variables = ref No let linux_ints = ref false let microsoft = ref false let extern_c = ref false +let short_names = ref true let extract_uints = ref false let builtin_uint128 = ref false