diff options
author | Son Ho | 2022-01-25 21:43:43 +0100 |
---|---|---|
committer | Son Ho | 2022-01-25 21:43:43 +0100 |
commit | 4789a0c1762dd8358b8c2f2b88653d0f9bf16059 (patch) | |
tree | 4f1eecc61a069ae8c99925f05ab6e306d489174c /src/SymbolicToPure.ml | |
parent | 31f6b09b7197bb934fcfda416b3a5f5056e5f4ad (diff) |
Make the back_id field non optional in Values.abs
Diffstat (limited to '')
-rw-r--r-- | src/SymbolicToPure.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 60fc8c7c..06ccf7bf 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -220,7 +220,7 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call) let bs_ctx_register_backward_call (abs : V.abs) (ctx : bs_ctx) : bs_ctx * fun_id = (* Insert the abstraction in the call informations *) - let back_id = Option.get abs.back_id in + let back_id = abs.back_id in let info = V.FunCallId.Map.find abs.call_id ctx.calls in assert (not (T.RegionGroupId.Map.mem back_id info.backwards)); let backwards = T.RegionGroupId.Map.add back_id abs info.backwards in @@ -233,7 +233,7 @@ let bs_ctx_register_backward_call (abs : V.abs) (ctx : bs_ctx) : bs_ctx * fun_id (* Retrieve the fun_id *) let fun_id = match info.forward.call_id with - | S.Fun (fid, _) -> Regular (fid, Some (Option.get abs.back_id)) + | S.Fun (fid, _) -> Regular (fid, Some abs.back_id) | S.Unop _ | S.Binop _ -> failwith "Unreachable" in (* Update the context and return *) @@ -669,9 +669,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : * *) (* First, retrieve the list of variables used for the inputs for the * backward function *) - let inputs = - T.RegionGroupId.Map.find (Option.get abs.back_id) ctx.backward_inputs - in + let inputs = T.RegionGroupId.Map.find abs.back_id ctx.backward_inputs in raise Unimplemented and translate_expansion (sv : V.symbolic_value) (exp : S.expansion) |