Feature #11772
closedUpdate CPAchecker
0%
Description
Anton just rebased his branch on the latest trunk, so we need to update CPAchecker in Klever and test it thoroughly.
Updated by Evgeny Novikov over 2 years ago
- Status changed from New to Resolved
I updated CPAchecker in branch update-cpachecker. Let's see on various testing results.
Updated by Evgeny Novikov over 2 years ago
- Status changed from Resolved to Open
- Memory safety:
- 2 safes -> 2 timeouts.
- 2 unsafes (target bug and false alarm) -> 2 timeouts.
- Non-memory safety:
- 3 unsafes (target bug and 2 false alarms) -> 3 timeouts.
It is necessary to figure out reasons of bad regressions at least for memory safety and fix them if possible.
Updated by Evgeny Novikov over 2 years ago
- Blocks Feature #11782: Update CIF added
Updated by Evgeny Novikov over 2 years ago
- Status changed from Open to Resolved
Anton has fixed some negative regressions, so I restarted CI.
Updated by Evgeny Novikov over 2 years ago
- Status changed from Resolved to Open
CI demonstrated numerous degradations. It seems that many (all) of them are caused by the same reason, so I hope that some fix will get rid of them.
Updated by Evgeny Novikov over 2 years ago
- Status changed from Open to Resolved
One more update of CPAchecker that should fix the issue is in the same branch. Let's see on testing results.
Updated by Evgeny Novikov over 2 years ago
- Status changed from Resolved to Open
The old issue has gone, but CI revealed a new large group of degradations that seem to stem from the same root cause:
Exception in thread "main" java.lang.NullPointerException at java.base/java.util.ArrayList.<init>(Unknown Source) at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.evaluateArgumentValue(SMGTransferRelation.java:459) at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.evaluateArgumentValues(SMGTransferRelation.java:425) at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.handleFunctionCallEdge(SMGTransferRelation.java:342) at org.sosy_lab.cpachecker.cpa.smg.SMGTransferRelation.handleFunctionCallEdge(SMGTransferRelation.java:114) 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)
Updated by Evgeny Novikov over 2 years ago
- Status changed from Open to Resolved
Anton has fixed the new issue, so I updated CPAchecker one more time and restarted CI.
Updated by Evgeny Novikov over 2 years ago
- Status changed from Resolved to Closed
CI regressions are described in c8ffc39. Verification of a subset of Linux 5.19-rc7 drivers demonstrated a pretty good speedup. Now more safes and unsafes can be found instead of timeouts and suspicious false alarms. SMG can not reveal several hard-to-detect safes anymore, but improvements are more considerable. I merged the branch to master in c8ffc391c.
Updated by Evgeny Novikov over 2 years ago
I forgot to mention that there is almost no changes for verification of those drivers against drivers:clk2.