summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/FunsAnalysis.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/FunsAnalysis.ml b/src/FunsAnalysis.ml
index 33f77f89..5a37a0a3 100644
--- a/src/FunsAnalysis.ml
+++ b/src/FunsAnalysis.ml
@@ -94,6 +94,7 @@ let analyze_module (m : llbc_module)
super#visit_Loop env loop
end
in
+ (* Sanity check: global bodies don't contain stateful calls *)
assert (not f.is_global_body || not !stateful);
(match f.body with
| None ->