summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-26 19:14:12 +0100
committerSon Ho2022-02-26 19:14:12 +0100
commit9f8deb8283fc5affdfc36218c22e316f0efb866f (patch)
treef5d7b8d171214b01c2085669c341fa6a6b4432c7
parent7063ad38f9da58f952bf4a47fbfae01163605000 (diff)
Add the betree_nll.rs test
Diffstat (limited to '')
-rw-r--r--Makefile13
-rw-r--r--tests/misc/BetreeNll.fst41
2 files changed, 54 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index ef8514ac..71488f23 100644
--- a/Makefile
+++ b/Makefile
@@ -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
+