Skip to content

SMG: Fix object inequality checks and value merge/replacement

Петров Олег Максимович requested to merge petrov-8take2-fix-areNotEqual into smg-master

Refactor objects comparison and value merge/replacement.

Unite checks 'an object cannot be the Null object' and general 'an object cannot be (i.e. overlap) another object' from AssumeVisitor and SMGState into private SMGState#areNotEqualObjects and use it in SMGState#areNonEqual(SMGValue, SMGValue), which is called in AssumeVisitor.

Note, an external object can be equal to Null if it has no has-value edges. Thus, two external objects can be equal only if they do not have HVEs, and their pointers are merged/replaced with 0 then (i.e. both objects are kind of replaced with Null). This branch closes #8 (closed).

Fix replacing 0 with another value (which drops 0->Null points-to edge too). Remove strange checks in replace(SMGValue, SMGValue).

Note, we consider 0-length lists not equal, which is unsound according to the FIT-TR-2012-04 (TODO use algorithms 12-13).

Edited by Петров Олег Максимович

Merge request reports