diff options
| -rw-r--r-- | src/FunsAnalysis.ml | 1 |
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 -> |