Merge pull request #343 from Nadrieril/update-charon

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.
-aec7312164f5f9d68ac432053f35e293de52ef01
+5642ea4f0e40ad4890f4e9dc69a500737ec08940

tests/coq/misc/External_FunsExternal_Template.v

@@ -12,15 +12,15 @@ Include External_Types.
 Module External_FunsExternal_Template.
 
 (** [core::cell::{core::cell::Cell<T>}#10::get]:
-    Source: '/rustc/library/core/src/cell.rs', lines 536:4-536:26
+    Source: '/rustc/library/core/src/cell.rs', lines 540:4-540:32
     Name pattern: core::cell::{core::cell::Cell<@T>}::get *)
 Axiom core_cell_Cell_get :
   forall{T : Type} (markerCopyInst : core_marker_Copy_t T),
         core_cell_Cell_t T -> state -> result (state * T)
 .
 
 (** [core::cell::{core::cell::Cell<T>}#11::get_mut]:
-    Source: '/rustc/library/core/src/cell.rs', lines 614:4-614:39
+    Source: '/rustc/library/core/src/cell.rs', lines 619:4-619:45
     Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *)
 Axiom core_cell_Cell_get_mut :
   forall{T : Type},
@@ -29,7 +29,7 @@ Axiom core_cell_Cell_get_mut :
 .
 
 (** [core::clone::Clone::clone_from]:
-    Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43
+    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),

tests/coq/misc/External_Types.v

@@ -11,7 +11,7 @@ Include External_TypesExternal.
 Module External_Types.
 
 (** Trait declaration: [core::marker::Copy]
-    Source: '/rustc/library/core/src/marker.rs', lines 404:0-404:21
+    Source: '/rustc/library/core/src/marker.rs', lines 416:0-416:21
     Name pattern: core::marker::Copy *)
 Record core_marker_Copy_t (Self : Type) := mkcore_marker_Copy_t {
   core_marker_Copy_tcore_marker_Copy_t_cloneCloneInst : core_clone_Clone Self;

tests/coq/misc/External_TypesExternal_Template.v

@@ -10,7 +10,7 @@ Local Open Scope Primitives_scope.
 Module External_TypesExternal_Template.
 
 (** [core::cell::Cell]
-    Source: '/rustc/library/core/src/cell.rs', lines 309:0-309:26
+    Source: '/rustc/library/core/src/cell.rs', lines 310:0-310:26
     Name pattern: core::cell::Cell *)
 Axiom core_cell_Cell_t : forall (T : Type), Type.
 

tests/fstar/misc/External.FunsExternal.fsti

@@ -7,22 +7,22 @@ include External.Types
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::cell::{core::cell::Cell<T>}#10::get]:
-    Source: '/rustc/library/core/src/cell.rs', lines 536:4-536:26
+    Source: '/rustc/library/core/src/cell.rs', lines 540:4-540:32
     Name pattern: core::cell::{core::cell::Cell<@T>}::get *)
 val core_cell_Cell_get
   (#t : Type0) (markerCopyInst : core_marker_Copy_t t) :
   core_cell_Cell_t t -> state -> result (state & t)
 
 (** [core::cell::{core::cell::Cell<T>}#11::get_mut]:
-    Source: '/rustc/library/core/src/cell.rs', lines 614:4-614:39
+    Source: '/rustc/library/core/src/cell.rs', lines 619:4-619:45
     Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut *)
 val core_cell_Cell_get_mut
   (#t : Type0) :
   core_cell_Cell_t t -> state -> result (state & (t & (t -> state -> result
     (state & (core_cell_Cell_t t)))))
 
 (** [core::clone::Clone::clone_from]:
-    Source: '/rustc/library/core/src/clone.rs', lines 175:4-175:43
+    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) :

tests/fstar/misc/External.Types.fst

@@ -7,7 +7,7 @@ include External.TypesExternal
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** Trait declaration: [core::marker::Copy]
-    Source: '/rustc/library/core/src/marker.rs', lines 404:0-404:21
+    Source: '/rustc/library/core/src/marker.rs', lines 416:0-416:21
     Name pattern: core::marker::Copy *)
 noeq type core_marker_Copy_t (self : Type0) = {
   cloneCloneInst : core_clone_Clone self;

tests/fstar/misc/External.TypesExternal.fsti

@@ -6,7 +6,7 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::cell::Cell]
-    Source: '/rustc/library/core/src/cell.rs', lines 309:0-309:26
+    Source: '/rustc/library/core/src/cell.rs', lines 310:0-310:26
     Name pattern: core::cell::Cell *)
 val core_cell_Cell_t (t : Type0) : Type0
 

tests/lean/External/FunsExternal_Template.lean

@@ -10,14 +10,14 @@ set_option linter.unusedVariables false
 open external
 
 /- [core::cell::{core::cell::Cell<T>}#10::get]:
-   Source: '/rustc/library/core/src/cell.rs', lines 536:4-536:26
+   Source: '/rustc/library/core/src/cell.rs', lines 540:4-540:32
    Name pattern: core::cell::{core::cell::Cell<@T>}::get -/
 axiom core.cell.Cell.get
   {T : Type} (markerCopyInst : core.marker.Copy T) :
   core.cell.Cell T → State → Result (State × T)
 
 /- [core::cell::{core::cell::Cell<T>}#11::get_mut]:
-   Source: '/rustc/library/core/src/cell.rs', lines 614:4-614:39
+   Source: '/rustc/library/core/src/cell.rs', lines 619:4-619:45
    Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut -/
 axiom core.cell.Cell.get_mut
   {T : Type} :

tests/lean/External/Types.lean

@@ -10,7 +10,7 @@ set_option linter.unusedVariables false
 namespace external
 
 /- Trait declaration: [core::marker::Copy]
-   Source: '/rustc/library/core/src/marker.rs', lines 404:0-404:21
+   Source: '/rustc/library/core/src/marker.rs', lines 416:0-416:21
    Name pattern: core::marker::Copy -/
 structure core.marker.Copy (Self : Type) where
   cloneCloneInst : core.clone.Clone Self

tests/lean/External/TypesExternal_Template.lean

@@ -8,7 +8,7 @@ set_option linter.hashCommand false
 set_option linter.unusedVariables false
 
 /- [core::cell::Cell]
-   Source: '/rustc/library/core/src/cell.rs', lines 309:0-309:26
+   Source: '/rustc/library/core/src/cell.rs', lines 310:0-310:26
    Name pattern: core::cell::Cell -/
 axiom core.cell.Cell (T : Type) : Type