summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/AssociatedTypes.ml12
-rw-r--r--compiler/InterpreterExpressions.ml7
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.ml4
-rw-r--r--compiler/InterpreterProjectors.ml2
-rw-r--r--compiler/PrintPure.ml6
-rw-r--r--compiler/PureMicroPasses.ml8
-rw-r--r--compiler/Substitute.ml2
-rw-r--r--compiler/SymbolicToPure.ml13
8 files changed, 29 insertions, 25 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml
index 083a38d1..27425a51 100644
--- a/compiler/AssociatedTypes.ml
+++ b/compiler/AssociatedTypes.ml
@@ -428,12 +428,12 @@ and norm_ctx_normalize_trait_instance_id (ctx : norm_ctx)
| TraitRef trait_ref ->
(* The trait instance id necessarily refers to a local sub-clause. We
can't project over it and can only peel off the [TraitRef] wrapper *)
- cassert_opt_meta __FILE__ __LINE__
+ sanity_check_opt_meta __FILE__ __LINE__
(trait_instance_id_is_local_clause trait_ref.trait_id)
- ctx.meta "Trait instance id is not a local sub-clause";
- cassert_opt_meta __FILE__ __LINE__
+ ctx.meta;
+ sanity_check_opt_meta __FILE__ __LINE__
(trait_ref.generics = empty_generic_args)
- ctx.meta "TODO: error message";
+ ctx.meta;
(trait_ref.trait_id, None)
| FnPointer ty ->
let ty = norm_ctx_normalize_ty ctx ty in
@@ -482,9 +482,9 @@ and norm_ctx_normalize_trait_ref (ctx : norm_ctx) (trait_ref : trait_ref) :
(lazy
("norm_ctx_normalize_trait_ref: normalized to: "
^ trait_ref_to_string ctx trait_ref));
- cassert_opt_meta __FILE__ __LINE__
+ sanity_check_opt_meta __FILE__ __LINE__
(generics = empty_generic_args)
- ctx.meta "TODO: error message";
+ ctx.meta;
trait_ref
(* Not sure this one is really necessary *)
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index d61ba410..48a1cce6 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -340,7 +340,9 @@ let eval_operand_no_reorganize (config : config) (meta : Meta.meta)
value_as_symbolic meta cv.value,
SymbolicAst.VaCgValue vid,
e )))
- | CFnPtr _ -> craise __FILE__ __LINE__ meta "TODO: error message")
+ | CFnPtr _ ->
+ craise __FILE__ __LINE__ meta
+ "Function pointers are not supported yet")
| Copy p ->
(* Access the value *)
let access = Read in
@@ -523,7 +525,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
* The remaining binops only operate on scalars. *)
if binop = Eq || binop = Ne then (
(* Equality operations *)
- exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta "TODO: error message";
+ exec_assert __FILE__ __LINE__ (v1.ty = v2.ty) meta
+ "The arguments given to the binop don't have the same type";
(* Equality/inequality check is primitive only for a subset of types *)
exec_assert __FILE__ __LINE__
(ty_is_primitively_copyable v1.ty)
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index 6d814c5c..bd271ff4 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -243,7 +243,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
(not
(ValuesUtils.value_has_borrows ctx0.type_ctx.type_infos
bv.value))
- M.meta "TODO: error message";
+ M.meta "The join of nested borrows is not supported yet";
let bid, bv =
M.match_mut_borrows ctx0 ctx1 ty bid0 bv0 bid1 bv1 bv
in
@@ -268,7 +268,7 @@ module MakeMatcher (M : PrimMatcher) : Matcher = struct
let sv = match_rec sv0 sv1 in
cassert __FILE__ __LINE__
(not (value_has_borrows sv.value))
- M.meta "TODO: error message";
+ M.meta "The join of nested borrows is not supported yet";
let ids, sv = M.match_shared_loans ctx0 ctx1 ty ids0 ids1 sv in
VSharedLoan (ids, sv)
| VMutLoan id0, VMutLoan id1 ->
diff --git a/compiler/InterpreterProjectors.ml b/compiler/InterpreterProjectors.ml
index d7c20ae0..8b6eeb6c 100644
--- a/compiler/InterpreterProjectors.ml
+++ b/compiler/InterpreterProjectors.ml
@@ -502,7 +502,7 @@ let apply_proj_borrows_on_input_value (config : config) (meta : Meta.meta)
(ctx : eval_ctx) (regions : RegionId.Set.t)
(ancestors_regions : RegionId.Set.t) (v : typed_value) (ty : rty) :
eval_ctx * typed_avalue =
- cassert __FILE__ __LINE__ (ty_is_rty ty) meta "TODO: error message";
+ sanity_check __FILE__ __LINE__ (ty_is_rty ty) meta;
let check_symbolic_no_ended = true in
let allow_reborrows = true in
(* Prepare the reborrows *)
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 518d8bdd..d0c243bb 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -411,7 +411,7 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
"Unreachable: improper variant id for result type"
| TError ->
cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta
- "TODO: error message";
+ "Ill-formed error value";
let variant_id = Option.get variant_id in
if variant_id = error_failure_id then "@Error::Failure"
else if variant_id = error_out_of_fuel_id then "@Error::OutOfFuel"
@@ -422,7 +422,7 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
let variant_id = Option.get variant_id in
if variant_id = fuel_zero_id then (
cassert_opt_meta __FILE__ __LINE__ (field_values = []) meta
- "TODO: error message";
+ "Ill-formed full value";
"@Fuel::Zero")
else if variant_id = fuel_succ_id then
match field_values with
@@ -435,7 +435,7 @@ let adt_g_value_to_string ?(meta : Meta.meta option = None) (env : fmt_env)
"Unreachable: improper variant id for fuel type"
| TArray | TSlice | TStr ->
cassert_opt_meta __FILE__ __LINE__ (variant_id = None) meta
- "TODO: error message";
+ "Ill-formed value";
let field_values =
List.mapi (fun i v -> string_of_int i ^ " -> " ^ v) field_values
in
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 91ee16dc..12b3387a 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1402,9 +1402,9 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
{ fwd_info; effect_info = loop_fwd_effect_info; ignore_output }
in
- cassert __FILE__ __LINE__
+ sanity_check __FILE__ __LINE__
(fun_sig_info_is_wf loop_fwd_sig_info)
- def.meta "TODO: error message";
+ def.meta;
let inputs_tys =
let fuel = if !Config.use_fuel then [ mk_fuel_ty ] else [] in
@@ -1444,10 +1444,10 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
(* Introduce the forward input state *)
let fwd_state_var, fwd_state_lvs =
- cassert __FILE__ __LINE__
+ sanity_check __FILE__ __LINE__
(loop_fwd_effect_info.stateful
= Option.is_some loop.input_state)
- def.meta "TODO: error message";
+ def.meta;
match loop.input_state with
| None -> ([], [])
| Some input_state ->
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index b9eebc25..177d8c24 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -77,7 +77,7 @@ let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta)
ctx_adt_get_instantiated_field_types ctx id adt.variant_id generics
| TTuple ->
cassert __FILE__ __LINE__ (generics.regions = []) meta
- "Regions should be empty TODO: error message";
+ "Tuples don't have region parameters";
generics.types
| TAssumed aty -> (
match aty with
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index ccb4f585..4830f65a 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -458,9 +458,7 @@ let rec translate_sty (meta : Meta.meta) (ty : T.ty) : ty =
match type_id with
| T.TAdtId adt_id -> TAdt (TAdtId adt_id, generics)
| T.TTuple ->
- cassert __FILE__ __LINE__
- (generics.const_generics = [])
- meta "TODO: error message";
+ sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta;
mk_simpl_tuple_ty generics.types
| T.TAssumed aty -> (
match aty with
@@ -486,7 +484,8 @@ let rec translate_sty (meta : Meta.meta) (ty : T.ty) : ty =
| TTraitType (trait_ref, type_name) ->
let trait_ref = translate_strait_ref meta trait_ref in
TTraitType (trait_ref, type_name)
- | TArrow _ -> craise __FILE__ __LINE__ meta "TODO: error message"
+ | TArrow _ ->
+ craise __FILE__ __LINE__ meta "Arrow types are not supported yet"
and translate_sgeneric_args (meta : Meta.meta) (generics : T.generic_args) :
generic_args =
@@ -659,7 +658,8 @@ let rec translate_fwd_ty (meta : Meta.meta) (type_infos : type_infos)
| TTraitType (trait_ref, type_name) ->
let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in
TTraitType (trait_ref, type_name)
- | TArrow _ -> craise __FILE__ __LINE__ meta "TODO: error message"
+ | TArrow _ ->
+ craise __FILE__ __LINE__ meta "Arrow types are not supported yet"
and translate_fwd_generic_args (meta : Meta.meta) (type_infos : type_infos)
(generics : T.generic_args) : generic_args =
@@ -768,7 +768,8 @@ let rec translate_back_ty (meta : Meta.meta) (type_infos : type_infos)
let trait_ref = translate_fwd_trait_ref meta type_infos trait_ref in
Some (TTraitType (trait_ref, type_name))
else None
- | TArrow _ -> craise __FILE__ __LINE__ meta "TODO: error message"
+ | TArrow _ ->
+ craise __FILE__ __LINE__ meta "Arrow types are not supported yet"
(** Simply calls [translate_back_ty] *)
let ctx_translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 14:19:09 +0000