diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 7 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 4 |
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 |