Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
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.
cb50ff16b9f1066b8a97dc06da704de2da2fa41c
527ea8e3b5dcb52edd6aef0f7bc34cc09c11dd59
22 changes: 19 additions & 3 deletions flake.lock

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

1 change: 1 addition & 0 deletions src/PrePasses.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1712,6 +1712,7 @@ let replace_static (crate : crate) : crate =
{
index = RegionId.of_int 1;
name = Some "'b";
variance = VaUnknown;
mutability = LtUnknown;
};
];
Expand Down
8 changes: 7 additions & 1 deletion src/interp/InterpUtils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -929,7 +929,13 @@ let instantiate_fun_sig (span : Meta.span option) (ctx : eval_ctx)
let fresh_regions = fresh_regions in
let fresh_region_vars : region_param list =
List.map
(fun index -> { Types.index; name = None; mutability = LtUnknown })
(fun index ->
{
Types.index;
name = None;
variance = VaUnknown;
mutability = LtUnknown;
})
fresh_regions
in
let open Substitute in
Expand Down
10 changes: 8 additions & 2 deletions src/llbc/Builtin.ml
Original file line number Diff line number Diff line change
Expand Up @@ -45,14 +45,20 @@ module Sig = struct

(** Region 'a of id 0 *)
let region_param_0 : region_param =
{ index = rvar_id_0; name = Some "'a"; mutability = LtUnknown }
{
index = rvar_id_0;
name = Some "'a";
variance = VaUnknown;
mutability = LtUnknown;
}

(** Region group: [{ parent={}; regions:{'a of id 0} }] *)
let region_group_0 : region_var_group =
{ id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] }

(** Type parameter [T] of id 0 *)
let type_param_0 : type_param = { index = tvar_id_0; name = "T" }
let type_param_0 : type_param =
{ index = tvar_id_0; name = "T"; variance = VaUnknown }

let usize_ty : ty = TLiteral (TUInt Usize)

Expand Down
2 changes: 1 addition & 1 deletion src/symbolic/SymbolicToPureTypes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -215,7 +215,7 @@ let translate_strait_type_constraint (span : Meta.span option)
{ trait_ref; type_id; ty }

let translate_type_param (p : T.type_param) : type_param =
let { index; name } : T.type_param = p in
let { index; name; variance = _ } : T.type_param = p in
{ index; name }

let translate_generic_params (span : Meta.span option)
Expand Down
Loading