summaryrefslogtreecommitdiff
path: root/compiler/Interpreter.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Interpreter.ml')
-rw-r--r--compiler/Interpreter.ml12
1 files changed, 12 insertions, 0 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index d0a54750..769e3144 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -191,6 +191,18 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
* do it, and because it gives a bit of sanity.
* *)
let sg = fdef.signature in
+ (* Sanity check: no nested borrows, borrows in ADTs, etc. *)
+ cassert __FILE__ __LINE__
+ (List.for_all
+ (fun ty -> not (ty_has_nested_borrows ctx.type_ctx.type_infos ty))
+ (sg.output :: sg.inputs))
+ fdef.meta "Nested borrows are not supported yet";
+ cassert __FILE__ __LINE__
+ (List.for_all
+ (fun ty -> not (ty_has_adt_with_borrows ctx.type_ctx.type_infos ty))
+ (sg.output :: sg.inputs))
+ fdef.meta "ADTs containing borrows are not supported yet";
+
(* Create the context *)
let regions_hierarchy =
FunIdMap.find (FRegular fdef.def_id) ctx.fun_ctx.regions_hierarchies