Merge pull request #59 from Nadrieril/update-charon

AeneasVerif · Aug 22, 2024 · cd5c9e5 · cd5c9e5
2 parents 67a59bf + 2c7e6df
commit cd5c9e5
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 24 deletions.
diff --git a/Makefile b/Makefile
@@ -1,7 +1,7 @@
 CHARON_HOME 	?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../charon
 KRML_HOME 	?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../karamel
 EURYDICE	?= ./eurydice $(EURYDICE_FLAGS)
-CHARON		?= $(CHARON_HOME)/bin/charon --extract-opaque-bodies
+CHARON		?= $(CHARON_HOME)/bin/charon
 
 BROKEN_TESTS		= step_by where_clauses chunks mutable_slice_range closure
 TEST_DIRS		= $(filter-out $(BROKEN_TESTS),$(subst test/,,$(shell find test -maxdepth 1 -mindepth 1 -type d)))

diff --git a/flake.lock b/flake.lock
diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml
@@ -750,22 +750,7 @@ let rec build_trait_clause_mapping env (trait_clauses : C.trait_clause list) =
             in
             ( (C.Clause clause_id, item_name),
               (decl_generics, ts, trait_decl.C.item_meta.name, decl.C.signature) ))
-          trait_decl.C.required_methods
-        @ List.map
-            (fun (item_name, decl_id) ->
-              match decl_id with
-              | Some decl_id ->
-                  let decl = env.get_nth_function decl_id in
-                  let ts =
-                    {
-                      K.n = List.length trait_decl.generics.types;
-                      n_cgs = List.length trait_decl.generics.const_generics;
-                    }
-                  in
-                  ( (C.Clause clause_id, item_name),
-                    (decl_generics, ts, trait_decl.C.item_meta.name, decl.C.signature) )
-              | None -> failwith ("TODO: handle provided trait methods, like " ^ item_name))
-            trait_decl.C.provided_methods
+          (trait_decl.C.required_methods @ trait_decl.C.provided_methods)
         @ List.flatten
             (List.mapi
                (fun i (parent_clause : C.trait_clause) ->