diff options
| -rw-r--r-- | Makefile | 18 | ||||
| -rw-r--r-- | flake.lock | 6 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain_Funs.v | 2 | ||||
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Funs.fst | 2 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 2 | ||||
| -rw-r--r-- | tests/lean/Betree.lean | 1 | ||||
| -rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 2 |
7 files changed, 17 insertions, 16 deletions
@@ -94,7 +94,7 @@ test: build-dev test-all test-all: test-no_nested_borrows test-paper \ test-hashmap test-hashmap_main \ test-external test-constants \ - testp-polonius_list testp-betree_main \ + test-polonius_list testp-betree_main \ ctest-testp-betree_main \ test-loops \ test-arrays test-traits test-bitwise test-demo @@ -183,14 +183,14 @@ tcoq-hashmap_main: OPTIONS += -use-fuel tlean-hashmap_main: SUBDIR := thol4-hashmap_main: OPTIONS += -testp-polonius_list: OPTIONS += -test-trans-units -testp-polonius_list: SUBDIR := misc -tfstarp-polonius_list: OPTIONS += -tcoqp-polonius_list: OPTIONS += -tleanp-polonius_list: SUBDIR := -tleanp-polonius_list: OPTIONS += -thol4p-polonius_list: SUBDIR := misc-polonius_list -thol4p-polonius_list: OPTIONS += +test-polonius_list: OPTIONS += -test-trans-units +test-polonius_list: SUBDIR := misc +tfstar-polonius_list: OPTIONS += +tcoq-polonius_list: OPTIONS += +tlean-polonius_list: SUBDIR := +tlean-polonius_list: OPTIONS += +thol4-polonius_list: SUBDIR := misc-polonius_list +thol4-polonius_list: OPTIONS += test-constants: OPTIONS += -test-trans-units test-constants: SUBDIR := misc @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1714045526, - "narHash": "sha256-ydEw01+8vnbGmgPXCXE22hJNRHUCJDnmU6yWlCvm2Ts=", + "lastModified": 1714483898, + "narHash": "sha256-R9c3HgcKZQq6VF7ZBjidiJTtxB2mYNJYxctD1JI7As0=", "owner": "aeneasverif", "repo": "charon", - "rev": "04b69a9251046115325bd67264cbcb999b0e8048", + "rev": "eb48f4a62ce7c330d44c1e3c870b2a7271bba73b", "type": "github" }, "original": { diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index c31713be..e0a1d8a2 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -827,7 +827,7 @@ Definition betree_BeTree_lookup . (** [betree_main::main]: - Source: 'src/betree_main.rs', lines 5:0-5:9 *) + Source: 'src/main.rs', lines 4:0-4:9 *) Definition main : result unit := Ok tt. diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index 89396df0..9942ef68 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -667,7 +667,7 @@ let betree_BeTree_lookup Ok (st1, (o, { self with root = n })) (** [betree_main::main]: - Source: 'src/betree_main.rs', lines 5:0-5:9 *) + Source: 'src/main.rs', lines 4:0-4:9 *) let main : result unit = Ok () diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index 89396df0..9942ef68 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -667,7 +667,7 @@ let betree_BeTree_lookup Ok (st1, (o, { self with root = n })) (** [betree_main::main]: - Source: 'src/betree_main.rs', lines 5:0-5:9 *) + Source: 'src/main.rs', lines 4:0-4:9 *) let main : result unit = Ok () diff --git a/tests/lean/Betree.lean b/tests/lean/Betree.lean new file mode 100644 index 00000000..58bee0c4 --- /dev/null +++ b/tests/lean/Betree.lean @@ -0,0 +1 @@ +import Betree.Funs diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index f0032d51..7cc52159 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -702,7 +702,7 @@ def betree.BeTree.lookup Result.ok (st1, (o, { self with root := n })) /- [betree_main::main]: - Source: 'src/betree_main.rs', lines 5:0-5:9 -/ + Source: 'src/main.rs', lines 4:0-4:9 -/ def main : Result Unit := Result.ok () |