Merge pull request #56 from Nadrieril/update-charon

AeneasVerif · Aug 14, 2024 · 9966247 · 9966247
2 parents 84e97e6 + 2fcb4fa
commit 9966247
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 9 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -91,6 +91,9 @@
           pkgs.ocamlPackages.ocaml
           pkgs.ocamlPackages.ocamlformat
           pkgs.ocamlPackages.menhir
+          # ocaml-lsp's version must match the ocaml version used. Pinning
+          # this here to save me a headache.
+          pkgs.ocamlPackages.ocaml-lsp
         ];
         buildInputs = [ charon.buildInputs ];
         nativeBuildInputs = [ charon.nativeBuildInputs fstar pkgs.clang ];

diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml
@@ -1583,7 +1583,7 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option =
       let env = push_type_binders env type_params in
 
       match kind with
-      | Opaque -> None
+      | Opaque | Error _-> None
       | Struct fields ->
           let fields =
             List.map

diff --git a/test/partial_eq/stubs.c b/test/partial_eq/stubs.c
@@ -1,6 +1,6 @@
 #include "partial_eq.h"
 
 extern core_result_Result_86
-core_fmt__core__fmt__Formatter__a__7__write_str(core_fmt_Formatter *x0, Prims_string x1) {
+core_fmt__core__fmt__Formatter__a__9__write_str(core_fmt_Formatter *x0, Prims_string x1) {
   return ((core_result_Result_86){ .tag = core_result_Ok, .f0 = NULL });
 }