From 6c9e4e52c6b42710843b88e92cad8b055998ed20 Mon Sep 17 00:00:00 2001 From: Timotej Kapus Date: Thu, 18 Jul 2019 03:05:43 -0700 Subject: [PATCH] [sledge][summaries] Fix unsoundes due to missing frame Summary: When using summaries we first garbage collect the precondition and then ask the solver to infer the frame of the precondition with respect to grabage-collected footprint. Currently if the solver fails to show the frame, we just give it an empty frame. This is bad, because if grabage collection removed some segments, they don't get added back on. This patch throws an exception instead to be very explicit when the solver cannot show the frame in this case. Reviewed By: ngorogiannis Differential Revision: D16339587 fbshipit-source-id: b88d0689c --- sledge/src/symbheap/state_domain.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml index 113492951..3c1ad8ea9 100644 --- a/sledge/src/symbheap/state_domain.ml +++ b/sledge/src/symbheap/state_domain.ml @@ -130,7 +130,9 @@ let call ~summaries actuals formals locals globals q = let pre = q' in let xs, foot = Sh.bind_exists ~wrt:pre.us foot in let frame = - Option.value ~default:Sh.emp (Solver.infer_frame pre xs foot) + Option.value_exn + (Solver.infer_frame pre xs foot) + ~message:"Solver couldn't infer frame of a garbage-collected pre" in let q'', subst = (Sh.extend_us locals (and_eqs formals actuals foot), freshen_locals)