From 855461700ef020cf402e3e452fc050f1a7be7a4c Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 6 Nov 2020 06:15:41 -0800 Subject: [PATCH] [sledge] Minor code simplification in Domain_sh.retn Reviewed By: da319 Differential Revision: D24746232 fbshipit-source-id: 19639328f --- sledge/src/domain_sh.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 7ec996f3b..34988aca2 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -210,7 +210,7 @@ let retn formals freturn {areturn; unshadow; frame} q = ; let formals = List.map ~f:X.reg formals in let freturn = Option.map ~f:X.reg freturn in - let q, shadows = + let q = match areturn with | Some areturn -> ( (* reenter scope of areturn just before exiting scope of formals *) @@ -218,16 +218,16 @@ let retn formals freturn {areturn; unshadow; frame} q = (* pass return value *) match freturn with | Some freturn -> - (Exec.move q (IArray.of_ (areturn, Term.var freturn)), unshadow) - | None -> (Exec.kill q areturn, unshadow) ) - | None -> (q, unshadow) + Exec.move q (IArray.of_ (areturn, Term.var freturn)) + | None -> Exec.kill q areturn ) + | None -> q in (* exit scope of formals *) let q = Sh.exists (Var.Set.add_list formals (Var.Set.of_option freturn)) q in (* reinstate shadowed values of locals *) - let q = Sh.rename shadows q in + let q = Sh.rename unshadow q in (* reconjoin frame *) Sh.star frame q (* simplify *)