diff options
author | Son HO | 2022-10-21 11:14:15 +0200 |
---|---|---|
committer | GitHub | 2022-10-21 11:14:15 +0200 |
commit | b4be489e7a5753bcc7f8714273ae71260fac53ce (patch) | |
tree | 45459740595bcdd70e5f4856b8499d1680d4ab91 /tests/misc/BetreePolonius.fst | |
parent | 53a2b8a2989485e8885d02c786206de84c9fd91d (diff) | |
parent | d62563cf9b8ef29ce20e810a5b1da999122c7a2f (diff) |
Merge pull request #4 from AeneasVerif/son_update_charon
Update the code to account for changes in Charon
Diffstat (limited to 'tests/misc/BetreePolonius.fst')
-rw-r--r-- | tests/misc/BetreePolonius.fst | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/tests/misc/BetreePolonius.fst b/tests/misc/BetreePolonius.fst new file mode 100644 index 00000000..2bac07b6 --- /dev/null +++ b/tests/misc/BetreePolonius.fst @@ -0,0 +1,41 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_polonius] *) +module BetreePolonius +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [betree_polonius::List] *) +type list_t (t : Type0) = +| ListCons : t -> list_t t -> list_t t +| ListNil : list_t t + +(** [betree_polonius::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_polonius::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 tl0 -> Return (ListCons hd tl0) + end + | ListNil -> Return ret + end + |