AssertionError (evaluation of parameters out of order) while validating a witness with SMG
I run witness validation using SMG (program, witness):
scripts/cpa.sh -64 \
-setprop witness.validation.violation.config=config/smg-ldv.properties \
-witness throwingWitness.graphml \
-spec config/properties/valid-memsafety.prp \
drivers--video--fbdev--udlfb.ko.i
It throws this AssertionError: evaluation of parameters out of order
both on my branch and on current smg-master.
See stack trace.
Exception in thread "main" java.lang.AssertionError: evaluation of parameters out of order
at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.evaluateArgumentValue(SMGTransferRelation.java:455)
at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.evaluateArgumentValues(SMGTransferRelation.java:422)
at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.handleFunctionCallEdge(SMGTransferRelation.java:338)
at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.handleFunctionCallEdge(SMGTransferRelation.java:112)
at org.sosy_lab.cpachecker.core.defaults.ForwardingTransferRelation.handleFunctionCallEdge(ForwardingTransferRelation.java:319)
at org.sosy_lab.cpachecker.core.defaults.ForwardingTransferRelation.getAbstractSuccessorsForEdge(ForwardingTransferRelation.java:169)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.callTransferRelation(CompositeTransferRelation.java:297)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForSimpleEdge(CompositeTransferRelation.java:264)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForEdge(CompositeTransferRelation.java:196)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessors(CompositeTransferRelation.java:88)
at org.sosy_lab.cpachecker.cpa.arg.ARGTransferRelation.getAbstractSuccessors(ARGTransferRelation.java:45)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(CPAAlgorithm.java:334)
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)