Merge pull request #248 from FStarLang/protz_no_short_names

New option: -fnoshort-names

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 ->

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 *)

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