From 5209b9976107592802327bac30e8b98fbb9c2d2f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 29 Apr 2024 13:37:38 +0200
Subject: Update charon
---
Makefile | 18 +++++++++---------
flake.lock | 6 +++---
tests/coq/betree/BetreeMain_Funs.v | 2 +-
tests/fstar/betree/BetreeMain.Funs.fst | 2 +-
tests/fstar/betree_back_stateful/BetreeMain.Funs.fst | 2 +-
tests/lean/Betree.lean | 1 +
tests/lean/BetreeMain/Funs.lean | 2 +-
7 files changed, 17 insertions(+), 16 deletions(-)
create mode 100644 tests/lean/Betree.lean
diff --git a/Makefile b/Makefile
index 08359d49..f4bb8f9e 100644
--- a/Makefile
+++ b/Makefile
@@ -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
diff --git a/flake.lock b/flake.lock
index b3b55e6f..014b0af1 100644
--- a/flake.lock
+++ b/flake.lock
@@ -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 ()
--
cgit v1.2.3