[pulse] also compare path conditions when comparing states

Summary:
States would be considered equal when they describe the same heap shape
even though their path conditions were different. Not good.

Reviewed By: skcho

Differential Revision: D26022135

fbshipit-source-id: 510913cde
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent abc36fe97f
commit d375a6c03e

@ -122,6 +122,7 @@ let leq ~lhs ~rhs =
phys_equal lhs rhs phys_equal lhs rhs
|| SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls || SkippedCalls.leq ~lhs:lhs.skipped_calls ~rhs:rhs.skipped_calls
&& ((not Config.pulse_isl) || equal_isl_status lhs.isl_status rhs.isl_status) && ((not Config.pulse_isl) || equal_isl_status lhs.isl_status rhs.isl_status)
&& PathCondition.equal lhs.path_condition rhs.path_condition
&& &&
match match
BaseDomain.isograph_map BaseDomain.empty_mapping BaseDomain.isograph_map BaseDomain.empty_mapping

Loading…
Cancel
Save