Add some missing error messages

3 files changed, 6 insertions, 9 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index ad204f7a..d6a5f0fc 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1876,11 +1876,8 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx)
 let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (global : global_decl) (body : fun_decl) (interface : bool) : unit =
   let meta = body.meta in
-  cassert __FILE__ __LINE__ body.is_global_decl_body body.meta
-    "TODO: Error message";
-  cassert __FILE__ __LINE__
-    (body.signature.inputs = [])
-    body.meta "TODO: Error message";
+  sanity_check __FILE__ __LINE__ body.is_global_decl_body body.meta;
+  sanity_check __FILE__ __LINE__ (body.signature.inputs = []) body.meta;
 
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break fmt 0 0;
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 6dbf528c..1f0abf8a 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -554,9 +554,9 @@ let rec extract_ty (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter)
         *)
         match trait_ref.trait_id with
         | Self ->
-            cassert __FILE__ __LINE__
+            sanity_check __FILE__ __LINE__
               (trait_ref.generics = empty_generic_args)
-              meta "TODO: Error message";
+              meta;
             extract_trait_instance_id_with_dot meta ctx fmt no_params_tys false
               trait_ref.trait_id;
             F.pp_print_string fmt type_name
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 7e6236b1..1cf1c5ef 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -440,7 +440,7 @@ let eval_box_new_concrete (config : config) (meta : Meta.meta)
       (* Required type checking *)
       cassert __FILE__ __LINE__
         (input_value.ty = boxed_ty)
-        meta "TODO: Error message";
+        meta "The input given to Box::new doesn't have the proper type";
 
       (* Move the input value *)
       let cf_move =
@@ -1431,7 +1431,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config)
          (fun ((arg, rty) : typed_value * rty) ->
            arg.ty = Subst.erase_regions rty)
          args_with_rtypes)
-      meta "TODO: Error message";
+      meta "The input arguments don't have the proper type";
     (* Check that the input arguments don't contain symbolic values that can't 
      * be fed to functions (i.e., symbolic values output from function return
      * values and which contain borrows of borrows can't be used as function