Add a test for divergence, Div.exe should reach a 1 second timeout

FStarLang · Sep 10, 2024 · 084979d · 084979d
1 parent 78f249a
commit 084979d
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 1 deletion.
diff --git a/tests/extraction/Div.fst b/tests/extraction/Div.fst
@@ -0,0 +1,7 @@
+module Div
+
+let rec f () : Dv int = f ()
+
+let _ =
+  let _ = f () in
+  1
diff --git a/tests/extraction/Makefile b/tests/extraction/Makefile
@@ -2,7 +2,7 @@ FSTAR_EXAMPLES=$(realpath ../../examples)
 include $(FSTAR_EXAMPLES)/Makefile.include
 include $(FSTAR_ULIB)/ml/Makefile.include
 
-all: inline_let all_cmi Eta_expand.test
+all: inline_let all_cmi Eta_expand.test Div.test
 
 %.exe: %.fst | out
 	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml $<
@@ -13,6 +13,13 @@ all: inline_let all_cmi Eta_expand.test
 	$(Q)./$<
 	$(Q)touch $@
 
+Div.test: Div.exe
+	$(call msg,TIMEOUT,$<)
+	$(Q)timeout 1 ./Div.exe ; \
+	  RC=$$? ;\
+	  if ! [ $$RC -eq 124 ]; then echo "ERROR: Div.exe terminated!?!?!"; false; fi
+	$(Q)touch $@
+
 inline_let: InlineLet.fst
 	$(FSTAR) --codegen OCaml InlineLet.fst
 	egrep -A 10 test InlineLet.ml | grep -qs "17"