Merge pull request #426 from Nadrieril/update-charon2

AeneasVerif · Jan 30, 2025 · 906d807 · 906d807
2 parents 21b296b + 620fa56
commit 906d807
Show file tree

Hide file tree

Showing 7 changed files with 12 additions and 56 deletions.
diff --git a/charon-pin b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-df3b7fd4c1277827c92b4a2cb84347f1f54d92a6
+ab692757d7033908c89bcc0e94d5ab1380b4f856
diff --git a/flake.lock b/flake.lock
diff --git a/scripts/update-charon-pin.sh b/scripts/update-charon-pin.sh
@@ -12,9 +12,6 @@ else
     echo 'Pinning the latest commit from Charon `main`'
     nix flake lock --update-input charon
 fi
-# In both cases we also update the rust overlay to make sure we can get the
-# latest rust nightlies.
-nix flake lock --update-input charon/rust-overlay
 
 # Keep the commit revision in `./charon-pin` as well so that non-nix users can know which commit to use.
 echo '# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.' > ./charon-pin

diff --git a/tests/coq/hashmap/Hashmap_FunsExternal_Template.v b/tests/coq/hashmap/Hashmap_FunsExternal_Template.v
@@ -19,12 +19,4 @@ Axiom utils_deserialize : state -> result (state * (HashMap_t u64)).
     Source: 'tests/src/hashmap.rs', lines 326:4-328:5 *)
 Axiom utils_serialize : HashMap_t u64 -> state -> result (state * unit).
 
-(** [core::clone::Clone::clone_from]:
-    Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43
-    Name pattern: core::clone::Clone::clone_from *)
-Axiom core_clone_Clone_clone_from :
-  forall{Self : Type} (self_clause : core_clone_Clone Self),
-        Self -> Self -> state -> result (state * Self)
-.
-
 End Hashmap_FunsExternal_Template.
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
@@ -28,12 +28,4 @@ Axiom core_cell_Cell_get_mut :
           (state * (core_cell_Cell_t T)))))
 .
 
-(** [core::clone::Clone::clone_from]:
-    Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43
-    Name pattern: core::clone::Clone::clone_from *)
-Axiom core_clone_Clone_clone_from :
-  forall{Self : Type} (self_clause : core_clone_Clone Self),
-        Self -> Self -> state -> result (state * Self)
-.
-
 End External_FunsExternal_Template.
diff --git a/tests/fstar/hashmap/Hashmap.FunsExternal.fsti b/tests/fstar/hashmap/Hashmap.FunsExternal.fsti
@@ -14,10 +14,3 @@ val utils_deserialize : state -> result (state & (hashMap_t u64))
     Source: 'tests/src/hashmap.rs', lines 326:4-328:5 *)
 val utils_serialize : hashMap_t u64 -> state -> result (state & unit)
 
-(** [core::clone::Clone::clone_from]:
-    Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43
-    Name pattern: core::clone::Clone::clone_from *)
-val core_clone_Clone_clone_from
-  (#self : Type0) (self_clause : core_clone_Clone self) :
-  self -> self -> state -> result (state & self)
-
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
@@ -21,10 +21,3 @@ val core_cell_Cell_get_mut
   core_cell_Cell_t t -> state -> result (state & (t & (t -> state -> (state &
     (core_cell_Cell_t t)))))
 
-(** [core::clone::Clone::clone_from]:
-    Source: '/rustc/library/core/src/clone.rs', lines 174:4-174:43
-    Name pattern: core::clone::Clone::clone_from *)
-val core_clone_Clone_clone_from
-  (#self : Type0) (self_clause : core_clone_Clone self) :
-  self -> self -> state -> result (state & self)
-