diff options
| -rw-r--r-- | Makefile | 13 | ||||
| -rw-r--r-- | tests/misc/BetreeNll.fst | 41 |
2 files changed, 54 insertions, 0 deletions
@@ -46,17 +46,30 @@ translate-nll-betree_nll: SUBDIR:=misc # The "standard" and the nll (non-linear lifetime) tests are in separate # directories in Charon .PHONY: gen-cfim-% + gen-cfim-%: CHARON_OPTIONS = --dest ../tests/cfim --no-code-duplication gen-cfim-%: CHARON_TESTS_SRC = ../tests/src + +gen-cfim-nll-%: CHARON_OPTIONS = --dest ../tests/cfim --no-code-duplication --nll +gen-cfim-nll-%: CHARON_TESTS_SRC = ../tests-nll/src + gen-cfim-%: build cd $(CHARON_HOME)/charon && cargo run $(CHARON_TESTS_SRC)/$*.rs $(CHARON_OPTIONS) +gen-cfim-nll-%: build + cd $(CHARON_HOME)/charon && cargo run $(CHARON_TESTS_SRC)/$*.rs $(CHARON_OPTIONS) + # Generic rule to test the translation on a CFIM file .PHONY: translate-% translate-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/cfim +translate-nll-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-nll/cfim + translate-%: gen-cfim-% dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.cfim -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) +translate-nll-%: gen-cfim-nll-% + dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.cfim -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) + .PHONY: doc doc: dune build @doc diff --git a/tests/misc/BetreeNll.fst b/tests/misc/BetreeNll.fst new file mode 100644 index 00000000..ae35827c --- /dev/null +++ b/tests/misc/BetreeNll.fst @@ -0,0 +1,41 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_nll] *) +module BetreeNll +open Primitives + +#set-options "--z3rlimit 50 --fuel 0 --ifuel 1" + +(** [betree_nll::List] *) +type list_t (t : Type0) = +| ListCons : t -> list_t t -> list_t t +| ListNil : list_t t + +(** [betree_nll::get_list_at_x] *) +let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) = + begin match ls with + | ListCons hd tl -> + if hd = x + then Return (ListCons hd tl) + else + begin match get_list_at_x_fwd tl x with + | Fail -> Fail + | Return l -> Return l + end + | ListNil -> Return ListNil + end + +(** [betree_nll::get_list_at_x] *) +let rec get_list_at_x_back + (ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) = + begin match ls with + | ListCons hd tl -> + if hd = x + then Return ret + else + begin match get_list_at_x_back tl x ret with + | Fail -> Fail + | Return l -> Return (ListCons hd l) + end + | ListNil -> Return ret + end + |