Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Change the criterion for KRML_IGNORE vs KRML_MAYBE_UNUSED_VAR #494

Merged
merged 2 commits into from
Oct 22, 2024
Merged

Change the criterion for KRML_IGNORE vs KRML_MAYBE_UNUSED_VAR #494

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
eb07ac3
New test case
msprotz Oct 22, 2024
e9e3440
Fixes #493
msprotz Oct 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion lib/UseAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
15 changes: 15 additions & 0 deletions test/KrmlTrue.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
7 changes: 6 additions & 1 deletion test/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down
Loading