diff --git a/lib/UseAnalysis.ml b/lib/UseAnalysis.ml index 1689cb06..cf75e97a 100644 --- a/lib/UseAnalysis.ml +++ b/lib/UseAnalysis.ml @@ -207,7 +207,7 @@ let use_mark_to_remove_or_ignore final = object (self) (* Definitely unused, except we can't generate let _ = ignore (bufcreate ...) -- this is a bad idea, as it'll force the hoisting phase to hoist the bufcreate back into a let-binding, which will then be named "buf". *) - else if not (is_bufcreate e1) then + else if not (is_bufcreate e1) && Helpers.is_value e1 then ELet ({ node = { b.node with meta = Some MetaSequence }; typ = TUnit; meta = []}, push_ignore e1, e2) diff --git a/test/KrmlTrue.fst b/test/KrmlTrue.fst new file mode 100644 index 00000000..0aa53ffb --- /dev/null +++ b/test/KrmlTrue.fst @@ -0,0 +1,15 @@ +module KrmlTrue + +let some_effectul_function (x:unit) : Dv unit = () + +let test (x:unit) +: Dv unit += let res = + let _ = some_effectul_function x in + true + in + some_effectul_function x + +let main () = + test (); + 0l diff --git a/test/Makefile b/test/Makefile index e66d88e5..7b04a8e4 100644 --- a/test/Makefile +++ b/test/Makefile @@ -60,7 +60,9 @@ 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-inline-let + check-right-file count-deref check-global-init check-useless-alias check-inline-let \ + check-comment check-ignore + ifneq ($(CRYPTO),) CRYPTO_WASM_FILES=Crypto.Symmetric.Chacha20.wasm-test endif @@ -247,6 +249,9 @@ check-comment: $(OUTPUT_DIR)/Comment.exe grep -q XXX3 $(OUTPUT_DIR)/Comment.out/Comment.c && \ true +check-ignore: $(OUTPUT_DIR)/KrmlTrue.exe + ! grep -q IGNORE $(OUTPUT_DIR)/KrmlTrue.out/KrmlTrue.c + clean: rm -rf $(WEB_DIR) .output