Skip to content

Update charon #491

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Nadrieril merged 1 commit into from
Apr 10, 2025
Merged

Update charon #491

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion charon-pin
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
ab02290d008d54f689aba42a626a251e5d328eae
142a6ad05bfa564dcf165e04660825ccf81ff2de
14 changes: 7 additions & 7 deletions flake.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 2 additions & 0 deletions src/symbolic/SymbolicToPure.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3194,6 +3194,8 @@ and translate_function_call_aux (call : S.call) (e : S.expression)
| CastTransmute _ ->
craise __FILE__ __LINE__ ctx.span "Unsupported: transmute"
end
| S.Unop E.PtrMetadata ->
craise __FILE__ __LINE__ ctx.span "Unsupported unop: PtrMetadata"
| S.Binop binop -> (
match args with
| [ arg0; arg1 ] ->
Expand Down
20 changes: 10 additions & 10 deletions tests/coq/misc/DefaultedMethod.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ Local Open Scope Primitives_scope.
Module DefaultedMethod.

(** [core::cmp::impls::{core::cmp::Ord for i32}#77::min]:
Source: '/rustc/library/core/src/cmp.rs', lines 1001:4-1003:20
Source: '/rustc/library/core/src/cmp.rs', lines 1048:4-1050:20
Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min] *)
Axiom core_cmp_impls_OrdI32_min : i32 -> i32 -> result i32.

Expand All @@ -20,7 +20,7 @@ Definition main : result unit :=
.

(** Trait declaration: [core::cmp::PartialEq]
Source: '/rustc/library/core/src/cmp.rs', lines 248:0-248:39
Source: '/rustc/library/core/src/cmp.rs', lines 249:0-249:39
Name pattern: [core::cmp::PartialEq] *)
Record core_cmp_PartialEq_t (Self : Type) (Rhs : Type)
:= mkcore_cmp_PartialEq_t {
Expand All @@ -31,7 +31,7 @@ Arguments mkcore_cmp_PartialEq_t { _ } { _ }.
Arguments core_cmp_PartialEq_t_eq { _ } { _ } _.

(** Trait declaration: [core::cmp::Eq]
Source: '/rustc/library/core/src/cmp.rs', lines 334:0-334:29
Source: '/rustc/library/core/src/cmp.rs', lines 335:0-335:29
Name pattern: [core::cmp::Eq] *)
Record core_cmp_Eq_t (Self : Type) := mkcore_cmp_Eq_t {
core_cmp_Eq_tcore_cmp_Eq_t_PartialEqInst : core_cmp_PartialEq_t Self Self;
Expand All @@ -41,7 +41,7 @@ Arguments mkcore_cmp_Eq_t { _ }.
Arguments core_cmp_Eq_tcore_cmp_Eq_t_PartialEqInst { _ } _.

(** [core::cmp::Ordering]
Source: '/rustc/library/core/src/cmp.rs', lines 387:0-387:17
Source: '/rustc/library/core/src/cmp.rs', lines 388:0-388:17
Name pattern: [core::cmp::Ordering] *)
Inductive core_cmp_Ordering_t :=
| Core_cmp_Ordering_Less : core_cmp_Ordering_t
Expand All @@ -50,7 +50,7 @@ Inductive core_cmp_Ordering_t :=
.

(** Trait declaration: [core::cmp::PartialOrd]
Source: '/rustc/library/core/src/cmp.rs', lines 1293:0-1293:56
Source: '/rustc/library/core/src/cmp.rs', lines 1340:0-1340:56
Name pattern: [core::cmp::PartialOrd] *)
Record core_cmp_PartialOrd_t (Self : Type) (Rhs : Type)
:= mkcore_cmp_PartialOrd_t {
Expand All @@ -66,7 +66,7 @@ Arguments core_cmp_PartialOrd_tcore_cmp_PartialOrd_t_PartialEqInst { _ } { _ }
Arguments core_cmp_PartialOrd_t_partial_cmp { _ } { _ } _.

(** Trait declaration: [core::cmp::Ord]
Source: '/rustc/library/core/src/cmp.rs', lines 946:0-946:36
Source: '/rustc/library/core/src/cmp.rs', lines 957:0-957:36
Name pattern: [core::cmp::Ord] *)
Record core_cmp_Ord_t (Self : Type) := mkcore_cmp_Ord_t {
core_cmp_Ord_tcore_cmp_Ord_t_EqInst : core_cmp_Eq_t Self;
Expand All @@ -83,27 +83,27 @@ Arguments core_cmp_Ord_t_cmp { _ } _.
Arguments core_cmp_Ord_t_min { _ } _.

(** [core::cmp::Ord::min]:
Source: '/rustc/library/core/src/cmp.rs', lines 1001:4-1003:20
Source: '/rustc/library/core/src/cmp.rs', lines 1048:4-1050:20
Name pattern: [core::cmp::Ord::min] *)
Axiom core_cmp_Ord_min_default :
forall{Self : Type} (self_clause : core_cmp_Ord_t Self),
Self -> Self -> result Self
.

(** [core::cmp::impls::{core::cmp::PartialEq<i32> for i32}#30::eq]:
Source: '/rustc/library/core/src/cmp.rs', lines 1636:16-1636:48
Source: '/rustc/library/core/src/cmp.rs', lines 1813:16-1813:50
Name pattern: [core::cmp::impls::{core::cmp::PartialEq<i32, i32>}::eq] *)
Axiom core_cmp_impls_PartialEqI32I32_eq : i32 -> i32 -> result bool.

(** [core::cmp::impls::{core::cmp::PartialOrd<i32> for i32}#76::partial_cmp]:
Source: '/rustc/library/core/src/cmp.rs', lines 1716:16-1716:69
Source: '/rustc/library/core/src/cmp.rs', lines 1928:16-1928:71
Name pattern: [core::cmp::impls::{core::cmp::PartialOrd<i32, i32>}::partial_cmp] *)
Axiom core_cmp_impls_PartialOrdI32I32_partial_cmp
: i32 -> i32 -> result (option core_cmp_Ordering_t)
.

(** [core::cmp::impls::{core::cmp::Ord for i32}#77::cmp]:
Source: '/rustc/library/core/src/cmp.rs', lines 1732:16-1732:53
Source: '/rustc/library/core/src/cmp.rs', lines 1938:16-1938:55
Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::cmp] *)
Axiom core_cmp_impls_OrdI32_cmp : i32 -> i32 -> result core_cmp_Ordering_t.

Expand Down
20 changes: 10 additions & 10 deletions tests/fstar/misc/DefaultedMethod.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"

(** [core::cmp::impls::{core::cmp::Ord for i32}#77::min]:
Source: '/rustc/library/core/src/cmp.rs', lines 1001:4-1003:20
Source: '/rustc/library/core/src/cmp.rs', lines 1048:4-1050:20
Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::min] *)
assume val core_cmp_impls_OrdI32_min : i32 -> i32 -> result i32

Expand All @@ -17,37 +17,37 @@ let main : result unit =
if n = 1 then Ok () else Fail Failure

(** Trait declaration: [core::cmp::PartialEq]
Source: '/rustc/library/core/src/cmp.rs', lines 248:0-248:39
Source: '/rustc/library/core/src/cmp.rs', lines 249:0-249:39
Name pattern: [core::cmp::PartialEq] *)
noeq type core_cmp_PartialEq_t (self : Type0) (rhs : Type0) = {
eq : self -> rhs -> result bool;
}

(** Trait declaration: [core::cmp::Eq]
Source: '/rustc/library/core/src/cmp.rs', lines 334:0-334:29
Source: '/rustc/library/core/src/cmp.rs', lines 335:0-335:29
Name pattern: [core::cmp::Eq] *)
noeq type core_cmp_Eq_t (self : Type0) = {
partialEqInst : core_cmp_PartialEq_t self self;
}

(** [core::cmp::Ordering]
Source: '/rustc/library/core/src/cmp.rs', lines 387:0-387:17
Source: '/rustc/library/core/src/cmp.rs', lines 388:0-388:17
Name pattern: [core::cmp::Ordering] *)
type core_cmp_Ordering_t =
| Core_cmp_Ordering_Less : core_cmp_Ordering_t
| Core_cmp_Ordering_Equal : core_cmp_Ordering_t
| Core_cmp_Ordering_Greater : core_cmp_Ordering_t

(** Trait declaration: [core::cmp::PartialOrd]
Source: '/rustc/library/core/src/cmp.rs', lines 1293:0-1293:56
Source: '/rustc/library/core/src/cmp.rs', lines 1340:0-1340:56
Name pattern: [core::cmp::PartialOrd] *)
noeq type core_cmp_PartialOrd_t (self : Type0) (rhs : Type0) = {
partialEqInst : core_cmp_PartialEq_t self rhs;
partial_cmp : self -> rhs -> result (option core_cmp_Ordering_t);
}

(** Trait declaration: [core::cmp::Ord]
Source: '/rustc/library/core/src/cmp.rs', lines 946:0-946:36
Source: '/rustc/library/core/src/cmp.rs', lines 957:0-957:36
Name pattern: [core::cmp::Ord] *)
noeq type core_cmp_Ord_t (self : Type0) = {
eqInst : core_cmp_Eq_t self;
Expand All @@ -57,25 +57,25 @@ noeq type core_cmp_Ord_t (self : Type0) = {
}

(** [core::cmp::Ord::min]:
Source: '/rustc/library/core/src/cmp.rs', lines 1001:4-1003:20
Source: '/rustc/library/core/src/cmp.rs', lines 1048:4-1050:20
Name pattern: [core::cmp::Ord::min] *)
assume val core_cmp_Ord_min_default
(#self : Type0) (self_clause : core_cmp_Ord_t self) :
self -> self -> result self

(** [core::cmp::impls::{core::cmp::PartialEq<i32> for i32}#30::eq]:
Source: '/rustc/library/core/src/cmp.rs', lines 1636:16-1636:48
Source: '/rustc/library/core/src/cmp.rs', lines 1813:16-1813:50
Name pattern: [core::cmp::impls::{core::cmp::PartialEq<i32, i32>}::eq] *)
assume val core_cmp_impls_PartialEqI32I32_eq : i32 -> i32 -> result bool

(** [core::cmp::impls::{core::cmp::PartialOrd<i32> for i32}#76::partial_cmp]:
Source: '/rustc/library/core/src/cmp.rs', lines 1716:16-1716:69
Source: '/rustc/library/core/src/cmp.rs', lines 1928:16-1928:71
Name pattern: [core::cmp::impls::{core::cmp::PartialOrd<i32, i32>}::partial_cmp] *)
assume val core_cmp_impls_PartialOrdI32I32_partial_cmp
: i32 -> i32 -> result (option core_cmp_Ordering_t)

(** [core::cmp::impls::{core::cmp::Ord for i32}#77::cmp]:
Source: '/rustc/library/core/src/cmp.rs', lines 1732:16-1732:53
Source: '/rustc/library/core/src/cmp.rs', lines 1938:16-1938:55
Name pattern: [core::cmp::impls::{core::cmp::Ord<i32>}::cmp] *)
assume val core_cmp_impls_OrdI32_cmp : i32 -> i32 -> result core_cmp_Ordering_t