Merge pull request #329 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.
-f1dc801340e4105927fe8f7be17b16ecaef78699
+cdc1dcde447a50cbc20336c79b21b42ac977b7fd

compiler/Extract.ml

@@ -2774,6 +2774,7 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
      * Extract the items
      *)
     let trait_decl_id = impl.impl_trait.trait_decl_id in
+    let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.crate.trait_decls in
 
     (* The constants *)
     List.iter
@@ -2810,19 +2811,19 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
       impl.types;
 
     (* The parent clauses *)
-    TraitClauseId.iteri
-      (fun clause_id trait_ref ->
+    List.iter
+      (fun (clause, trait_ref) ->
         let item_name =
           ctx_get_trait_parent_clause impl.item_meta.span trait_decl_id
-            clause_id ctx
+            clause.T.clause_id ctx
         in
         let ty () =
           F.pp_print_space fmt ();
           extract_trait_ref impl.item_meta.span ctx fmt TypeDeclId.Set.empty
             false trait_ref
         in
         extract_trait_impl_item ctx fmt item_name ty)
-      impl.parent_trait_refs;
+      (List.combine trait_decl.parent_clauses impl.parent_trait_refs);
 
     (* The required methods *)
     List.iter

flake.nix

@@ -90,7 +90,7 @@
         betree-llbc = charon.extractCrateWithCharon.${system} {
           name = "betree";
           src = ./tests/src/betree;
-          charonFlags = "--polonius --opaque=crate::betree_utils";
+          charonFlags = "--polonius --opaque=crate::betree_utils --hide-marker-traits";
           craneExtraArgs.checkPhaseCargoCommand = ''
             cargo rustc -- --test -Zpolonius
             ./target/debug/betree

tests/test_runner/run_test.ml

@@ -117,6 +117,7 @@ let run_charon (env : runner_env) (case : Input.t) =
         [
           env.charon_path;
           "--no-cargo";
+          "--hide-marker-traits";
           "--input";
           case.path;
           "--crate";
@@ -143,7 +144,12 @@ let run_charon (env : runner_env) (case : Input.t) =
       in
       if generate then (
         let args =
-          [ env.charon_path; "--dest"; Filename_unix.realpath env.llbc_dir ]
+          [
+            env.charon_path;
+            "--hide-marker-traits";
+            "--dest";
+            Filename_unix.realpath env.llbc_dir;
+          ]
         in
         let args = List.append args case.charon_options in
         (* Run Charon inside the crate *)