diff options
| author | Son HO | 2024-01-25 12:03:38 +0100 |
|---|---|---|
| committer | GitHub | 2024-01-25 12:03:38 +0100 |
| commit | 202f0153dc51983e6bc0eddb65d22c763579850c (patch) | |
| tree | d948f1104170d7254e8802eb7bf2b77a4386d3b3 /compiler/InterpreterLoops.ml | |
| parent | 15a7d7b7322a1cd0ebeb328fde214060e23fa8b4 (diff) | |
| parent | d89cbfdc3f972e1ff4c7c9dd723146556d26526d (diff) | |
Merge pull request #65 from AeneasVerif/son/fix_loops
Fix an issue with loops
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterLoops.ml | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index ed2a9587..6ee08e47 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -93,10 +93,20 @@ let eval_loop_symbolic (config : config) (meta : meta) let fp_bl_corresp = compute_fixed_point_id_correspondance fixed_ids ctx fp_ctx in - let end_expr = + log#ldebug + (lazy + ("eval_loop_symbolic: about to match the fixed-point context with the \ + original context:\n\ + - src ctx (fixed-point ctx)" ^ eval_ctx_to_string fp_ctx + ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx)); + let end_expr : SymbolicAst.expression option = match_ctx_with_target config loop_id true fp_bl_corresp fp_input_svalues fixed_ids fp_ctx cf ctx in + log#ldebug + (lazy + "eval_loop_symbolic: matched the fixed-point context with the original \ + context"); (* Synthesize the loop body by evaluating it, with the continuation for after the loop starting at the *fixed point*, but with a special @@ -115,6 +125,12 @@ let eval_loop_symbolic (config : config) (meta : meta) | Continue i -> (* We don't support nested loops for now *) assert (i = 0); + log#ldebug + (lazy + ("eval_loop_symbolic: about to match the fixed-point context with \ + the context at a continue:\n\ + - src ctx (fixed-point ctx)" ^ eval_ctx_to_string fp_ctx + ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string ctx)); let cc = match_ctx_with_target config loop_id false fp_bl_corresp fp_input_svalues fixed_ids fp_ctx |