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.