[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
master
Timotej Kapus 5 years ago committed by Facebook Github Bot
parent 937e971849
commit 6c9e4e52c6

@ -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)

Loading…
Cancel
Save