SMG-LDV: problem in join sub-SMGs
This command quickly results in a crash on smg-master branch:
scripts/cpa.sh -smg-ldv -preprocess test/programs/cpalien/0012-trivial-tree.c
But analysis with -smg
quickly finds an error.
SMGJoinValues.insertLeftListAndJoin:1130
gets two edges for some reason.
See full trace.
Exception in thread "main" java.lang.IllegalArgumentException: expected one element but was: <Sym_25->sll+0b, Sym_59->sll+0b>
at com.google.common.collect.Iterators.getOnlyElement(Iterators.java:323)
at com.google.common.collect.Iterables.getOnlyElement(Iterables.java:263)
at org.sosy_lab.cpachecker.cpa.smg.SMGState.getAddress(SMGState.java:1736)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinValues.insertLeftListAndJoin(SMGJoinValues.java:1130)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinValues.<init>(SMGJoinValues.java:318)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinSubSMGs.<init>(SMGJoinSubSMGs.java:143)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinTargetObjects.<init>(SMGJoinTargetObjects.java:189)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinValues.joinValuesPointers(SMGJoinValues.java:198)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinValues.<init>(SMGJoinValues.java:297)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinSubSMGs.<init>(SMGJoinSubSMGs.java:143)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoin.<init>(SMGJoin.java:115)
at org.sosy_lab.cpachecker.cpa.smg.SMGState.isLessOrEqual(SMGState.java:1529)
at org.sosy_lab.cpachecker.cpa.smg.SMGState.isLessOrEqual(SMGState.java:90)
at org.sosy_lab.cpachecker.core.defaults.DelegateAbstractDomain.isLessOrEqual(DelegateAbstractDomain.java:40)
at org.sosy_lab.cpachecker.core.defaults.StopSepOperator.stop(StopSepOperator.java:33)
at org.sosy_lab.cpachecker.cpa.smg.SMGStopOperator.stop(SMGStopOperator.java:30)
at org.sosy_lab.cpachecker.cpa.composite.CompositeStopOperator.stop(CompositeStopOperator.java:67)
at org.sosy_lab.cpachecker.cpa.composite.CompositeStopOperator.stop(CompositeStopOperator.java:40)
at org.sosy_lab.cpachecker.cpa.arg.ARGStopSep.stop(ARGStopSep.java:148)
at org.sosy_lab.cpachecker.cpa.arg.ARGStopSep.stop(ARGStopSep.java:111)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(CPAAlgorithm.java:451)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run0(CPAAlgorithm.java:289)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run(CPAAlgorithm.java:260)
at org.sosy_lab.cpachecker.core.algorithm.CounterexampleStoreAlgorithm.run(CounterexampleStoreAlgorithm.java:58)
at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:512)
at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:377)
at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:170)