diff options
| author | Son HO | 2022-09-22 16:29:32 +0200 |
|---|---|---|
| committer | GitHub | 2022-09-22 16:29:32 +0200 |
| commit | 573dc89a52224be4c0887ae98d677305605b0539 (patch) | |
| tree | 5f68498b84c46661b9f14a934eaa4ed6be5abfec /src/FunsAnalysis.ml | |
| parent | 692babd59421995809ce0cf7d4354a591dc73fe3 (diff) | |
Update src/FunsAnalysis.ml
Diffstat (limited to '')
| -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 -> |