diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/FunsAnalysis.ml | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index f6976f23..f194d4e5 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -9,6 +9,7 @@ open LlbcAst open ExpressionsUtils +open Errors (** Various information about a function. @@ -36,7 +37,6 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) (globals_map : global_decl GlobalDeclId.Map.t) (use_state : bool) : modules_funs_info = let infos = ref FunDeclId.Map.empty in - let register_info (id : FunDeclId.id) (info : fun_info) : unit = assert (not (FunDeclId.Map.mem id !infos)); infos := FunDeclId.Map.add id info !infos @@ -145,7 +145,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) end in (* Sanity check: global bodies don't contain stateful calls *) - assert ((not f.is_global_decl_body) || not !stateful); + cassert __FILE__ __LINE__ + ((not f.is_global_decl_body) || not !stateful) + f.meta "Global definition containing a stateful call in its body"; let builtin_info = get_builtin_info f in let has_builtin_info = builtin_info <> None in group_has_builtin_info := !group_has_builtin_info || has_builtin_info; @@ -167,8 +169,15 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) (* We need to know if the declaration group contains a global - note that * groups containing globals contain exactly one declaration *) let is_global_decl_body = List.exists (fun f -> f.is_global_decl_body) d in - assert ((not is_global_decl_body) || List.length d = 1); - assert ((not !group_has_builtin_info) || List.length d = 1); + cassert __FILE__ __LINE__ + ((not is_global_decl_body) || List.length d = 1) + (List.hd d).meta + "This global definition is in a group of mutually recursive definitions"; + cassert __FILE__ __LINE__ + ((not !group_has_builtin_info) || List.length d = 1) + (List.hd d).meta + "This builtin function belongs to a group of mutually recursive \ + definitions"; (* We ignore on purpose functions that cannot fail and consider they *can* * fail: the result of the analysis is not used yet to adjust the translation * so that the functions which syntactically can't fail don't use an error monad. |