-fno-shadow, to defeat some of MSVC's default warnings about shadowin…

…g a declaration of a different type

_tags

@@ -8,5 +8,5 @@ true: annot, bin_annot, warn(@1-2-3@8..12@14..21@23..29-30@31..38-39@40-41@43@57
   package(visitors.ppx), package(visitors.runtime)
 "parser/Lexer.ml": syntax(camlp4o), syntax(pa_ulex)
 <test>: -traverse
-<kremlib/{extracted,c,out}>: -traverse
+<kremlib/{extracted,c,out,uint128}>: -traverse
 <kremlib/**/*.ml>: package(fstarlib)

src/AstToCStar.ml

@@ -134,7 +134,8 @@ let ensure_fresh env name body cont =
   mk_fresh name (fun tentative ->
     tricky_shadowing_see_comment_above tentative body 0 ||
     List.exists (fun cont -> tricky_shadowing_see_comment_above tentative (Some cont) 1) cont ||
-    List.exists ((=) tentative) env.in_block)
+    List.mem tentative env.in_block ||
+    !Options.no_shadow && List.mem tentative env.names)
 
 
 (** AstToCStar performs a unit-to-void conversion.

src/Kremlin.ml

@@ -237,6 +237,8 @@ Supported options:|}
       loops smaller than N";
     "-fparentheses", Arg.Set Options.parentheses, "  add unnecessary parentheses \
       to silence GCC and Clang's -Wparentheses";
+    "-fno-shadow", Arg.Set Options.no_shadow, "  add unnecessary renamings to \
+      defeat GCC and Clang's -Wshadow, as well as the various MSVC warnings";
     "-fcurly-braces", Arg.Set Options.curly_braces, "  always add curly braces \
       around blocks";
     "-fshort-enums", Arg.Set Options.short_enums, "  use C macros and uint8_t \

src/Options.ml

@@ -40,6 +40,7 @@ let parentheses = ref false
 let curly_braces = ref false
 let unroll_loops = ref (-1)
 let tail_calls = ref false
+let no_shadow = ref false
 
 let extract_uint128 = ref false
 

test/Makefile

@@ -20,7 +20,7 @@ FILES		= \
   Verbatim.test Const.test $(CRYPTO)/Crypto.Symmetric.Chacha20.test Uu.test \
   LinkedList1.test LinkedList2.test LinkedList3.test LinkedList4.test \
   NoExtract.test InlineNoExtract.test ../book/RingBuffer.test \
-  ../book/Introduction.test TopLevelArray.test
+  ../book/Introduction.test TopLevelArray.test NoShadow.test
 CUSTOM		= count-uu
 WASM_FILES	= \
   WasmTrap.wasm-test Wasm1.wasm-test Wasm2.wasm-test Wasm3.wasm-test Wasm4.wasm-test
@@ -105,6 +105,7 @@ $(OUTPUT_DIR)/TotalLoops.exe: EXTRA = -add-include '"kremlin/internal/compat.h"'
 $(OUTPUT_DIR)/CheckedInt.exe: EXTRA = -add-include '"kremlin/internal/compat.h"'
 $(OUTPUT_DIR)/CustomEq.exe: EXTRA = -add-include '"kremlin/internal/compat.h"'
 $(OUTPUT_DIR)/DataTypes.exe: EXTRA = -fshort-enums
+$(OUTPUT_DIR)/NoShadow.exe: EXTRA = -ccopt -Wshadow -fno-shadow
 
 # Some custom targets
 

test/NoShadow.fst

@@ -0,0 +1,32 @@
+module NoShadow
+
+module U32 = FStar.UInt32
+module U64 = FStar.UInt64
+module HS = FStar.HyperStack
+
+open FStar.HyperStack.ST
+
+let f x: StackInline unit (fun _ -> true) (fun _ _ _ -> true) =
+  let x = U32.(x +%^ 1ul) in
+  TestLib.checku32 x 1ul
+
+let g x: StackInline unit (fun _ -> true) (fun _ _ _ -> true) =
+  let x = U64.(x +%^ 1UL) in
+  TestLib.checku64 x 1UL
+
+let b (): Stack bool (fun _ -> true) (fun _ _ _ -> true) =
+  true
+
+let h x y: Stack unit (fun _ -> true) (fun _ _ _ -> true) =
+  push_frame ();
+  if b () then begin
+    f x;
+    if b () then begin
+      g y
+    end
+  end;
+  pop_frame ()
+
+let main (): Stack Int32.t (fun _ -> true) (fun _ _ _ -> true) =
+  h 0ul 0UL;
+  0l