diff options
| author | Son HO | 2024-03-29 18:02:40 +0100 |
|---|---|---|
| committer | GitHub | 2024-03-29 18:02:40 +0100 |
| commit | f4a89caad1459f2f72295c5baa284fe1f9b4c39f (patch) | |
| tree | 70237cbc5ff7e0868c9b6918cae21f9bc8ba6272 /compiler/InterpreterLoopsJoinCtxs.mli | |
| parent | bfcec191f68a4cbfab14f5b92a8d6a46d6b02539 (diff) | |
| parent | 1a86cac476c1f5c0d64d5a12db267d3ac651561b (diff) | |
Merge pull request #95 from AeneasVerif/escherichia/errors
Escherichia/errors
Diffstat (limited to 'compiler/InterpreterLoopsJoinCtxs.mli')
| -rw-r--r-- | compiler/InterpreterLoopsJoinCtxs.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/compiler/InterpreterLoopsJoinCtxs.mli b/compiler/InterpreterLoopsJoinCtxs.mli index bb9f14ed..0e84657c 100644 --- a/compiler/InterpreterLoopsJoinCtxs.mli +++ b/compiler/InterpreterLoopsJoinCtxs.mli @@ -16,6 +16,7 @@ open InterpreterLoopsCore - [aid1] *) val merge_into_abstraction : + Meta.meta -> loop_id -> abs_kind -> bool -> @@ -84,7 +85,8 @@ val merge_into_abstraction : - [ctx0] - [ctx1] *) -val join_ctxs : loop_id -> ids_sets -> eval_ctx -> eval_ctx -> ctx_or_update +val join_ctxs : + Meta.meta -> loop_id -> ids_sets -> eval_ctx -> eval_ctx -> ctx_or_update (** Join the context at the entry of the loop with the contexts upon reentry (upon reaching the [Continue] statement - the goal is to compute a fixed @@ -104,6 +106,7 @@ val join_ctxs : loop_id -> ids_sets -> eval_ctx -> eval_ctx -> ctx_or_update *) val loop_join_origin_with_continue_ctxs : config -> + Meta.meta -> loop_id -> ids_sets -> eval_ctx -> |