Skip to content

IllegalArgumentException at SMGJoinMatchObjects.java:121 after fixes in marchenko-smg-abstraction branch

After fixes in marchenko_smg_abstraction branch the test test/programs/smg_abstraction_tests/sll/sll_subsmg/sll_subsmg.c fails with an error: Exception in thread "main" java.lang.IllegalArgumentException at com.google.common.base.Preconditions.checkArgument(Preconditions.java:131) at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinMatchObjects.<init>(SMGJoinMatchObjects.java:121).

Test runs with the following parameters: scripts/cpa.sh -smg-ldv -preprocess -spec test/config/properties/valid-memsafety.prp -setprop cpa.smg.seqLengthEntailmentThreshold=2 -setprop cpa.smg.seqLengthEqualityThreshold=2 -setprop cpa.smg.seqLengthIncomparableThreshold=2 test/programs/smg_abstraction_tests/sll/sll_subsmg/sll_subsmg.c

The reason of the exception is abstraction sequence length = 2, so with other sequence lengths the result is True. This happens because of SMGKnownAddressValue type which contains concrete object after list materialization, so due to abstraction with length equal to 2 an abstraction of a concrete element with a list occurs. But SMGKnownAddressValue value continues to reference this concrete object.

In master branch before all fixes from marchenko_smg_abstraction we had verdict FALSE instead of correct TRUE with abstraction sequence length equals to 2, and UNKNOWN with SMG inconsistent: inconsistent edges on all abstraction sequence lengths if cpa.smg.runtimeCheck=FULL is enabled.