diff options
| author | Son Ho | 2022-11-09 22:47:13 +0100 |
|---|---|---|
| committer | Son HO | 2022-11-10 11:35:30 +0100 |
| commit | fac185188ff0969cc5012c71f9d50871800e3f41 (patch) | |
| tree | f63f4b8b09d26ce6f82aec0fd84c285bd5f40eee /compiler/SynthesizeSymbolic.ml | |
| parent | 4ec8646c1bf426c848e8057cdf7c248df6999523 (diff) | |
Factor out the symbolic execution for the forward/backward translations
Diffstat (limited to 'compiler/SynthesizeSymbolic.ml')
| -rw-r--r-- | compiler/SynthesizeSymbolic.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 8d4dac82..5bcbd482 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -152,5 +152,6 @@ let synthesize_assignment (lplace : mplace) (rvalue : V.typed_value) let synthesize_assertion (v : V.typed_value) (e : expression option) = Option.map (fun e -> Assertion (v, e)) e -let synthesize_forward_end (e : expression option) = - Option.map (fun e -> ForwardEnd e) e +let synthesize_forward_end (e : expression) + (el : expression T.RegionGroupId.Map.t) = + Some (ForwardEnd (e, el)) |