diff --git a/tests/extraction/Div.fst b/tests/extraction/Div.fst new file mode 100644 index 00000000000..ef5bf840dca --- /dev/null +++ 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 index 790724536b8..84952c9372c 100644 --- 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"