From 2b17f28bfd42e4de6f9db91448ce4e97d03ae5cc Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 10 May 2022 23:04:25 +0200 Subject: [PATCH] More filtering of Steel modules --- test/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Makefile b/test/Makefile index 22185d1b8..f4c0f4396 100644 --- a/test/Makefile +++ b/test/Makefile @@ -69,7 +69,7 @@ ifndef NODEPEND # AF: The Steel files should not be extracted by KaRaMeL, they are filtered out .depend: .FORCE $(FSTAR) --dep full $(subst .wasm-test,.fst,$(WASM_FILES)) $(subst .test,.fst,$(FILES)) \ - $(BROKEN) ../runtime/WasmSupport.fst --extract 'krml:*,-Prims,-FStar.MSTTotal,-FStar.NMSTTotal,-FStar.MST,-FStar.NMST,-Steel' > $@ + $(BROKEN) ../runtime/WasmSupport.fst --extract 'krml:*,-Prims,-FStar.MSTTotal,-FStar.NMSTTotal,-FStar.MST,-FStar.NMST,-Steel.Effect,-Steel.Effect.Atomic,-Steel.HigherReference,-Steel.Reference,-Steel.Semantics.Hoare.MST' > $@ .PHONY: .FORCE .FORCE: