summaryrefslogtreecommitdiff
path: root/compiler/FunsAnalysis.ml
diff options
context:
space:
mode:
authorNadrieril2024-06-21 15:47:56 +0200
committerNadrieril2024-06-21 16:14:58 +0200
commitd3f52e23ede39c4fd7845b6c5feb29d28b2a2384 (patch)
tree2891753ba71bc8ddd3cc367b787a1acddbcf1741 /compiler/FunsAnalysis.ml
parentc8ad44f287215c3c45e5a0f0540ef507b4916c7d (diff)
Update charon
Diffstat (limited to '')
-rw-r--r--compiler/FunsAnalysis.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index 815c470f..e0a86145 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -223,6 +223,13 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
let global = GlobalDeclId.Map.find id globals_map in
analyze_fun_decl_group (NonRecGroup global.body);
analyze_decl_groups decls'
+ | MixedGroup ids :: _ ->
+ craise_opt_span __FILE__ __LINE__ None
+ ("Mixed declaration groups are not supported yet: ["
+ ^ String.concat ", "
+ (List.map Charon.PrintGAst.any_decl_id_to_string
+ (Charon.GAstUtils.g_declaration_group_to_list ids))
+ ^ "]")
in
analyze_decl_groups m.declarations;