Add a test for @@cinline on letbinding

test/InlineLet.fst

@@ -0,0 +1,14 @@
+module InlineLet
+
+(* None of {foobar,temp_x,temp_y} should appear in the output *)
+
+let main () =
+  let open FStar.Int32 in
+  [@@CInline] let foobar = 0l in
+  add foobar 0l
+
+let foo (a:UInt32.t) =
+  let open FStar.UInt32 in
+  [@@CInline] let temp_x = a in
+  [@@CInline] let temp_y = a in
+  temp_x `add_underspec` temp_y

test/Makefile

@@ -60,7 +60,7 @@ ifneq ($(RECENT_GCC),"yes")
 endif
 
 CUSTOM		= count-eq count-uu check-unused check-no-constructor check-no-erased \
-  check-right-file count-deref check-global-init check-useless-alias
+  check-right-file count-deref check-global-init check-useless-alias check-inline-let
 ifneq ($(CRYPTO),)
   CRYPTO_WASM_FILES=Crypto.Symmetric.Chacha20.wasm-test
 endif
@@ -236,6 +236,11 @@ check-no-erased: $(OUTPUT_DIR)/Shifting.exe
 check-right-file: $(OUTPUT_DIR)/MonomorphizationSeparate2.exe
 	egrep -q 'typedef.*pair' $(OUTPUT_DIR)/MonomorphizationSeparate2.out/MonomorphizationSeparate1.h
 
+check-inline-let: $(OUTPUT_DIR)/InlineLet.exe
+	! grep foobar $(OUTPUT_DIR)/InlineLet.out/InlineLet.c
+	! grep temp_x $(OUTPUT_DIR)/InlineLet.out/InlineLet.c
+	! grep temp_y $(OUTPUT_DIR)/InlineLet.out/InlineLet.c
+
 clean:
 	rm -rf $(WEB_DIR) .output