Feature #8897
closed
- Status changed from New to Resolved
Implemented in 8897-trunk-cpachecker. Updated CPAchecker in Klever for SMG and reachability up to 27946 of trunk.
- Status changed from Resolved to Open
Also I updated CPALockator to CPALockator:26692 in d348f5cb to branch 8897-trunk-cpachecker.
But it turns out that a new version of CPAchecker from trunk results into too many failures when processing its witnesses produced for Klever tests. So, we need to understand who is wrong and to fix them.
I fixed the most of cases but there is one important: CPAchecker does not print warning edge which is extremly important for applying marks. So lets wait a bit for fixes.
Current progress in available in 8897-trunk-cpachecker and in core-new-formats (with Django2 support).
Regarding warning edge
1. CPAchecker does not print it for reachability and it is a correct behavior
2. For printing the last edge with call to __VERIFIER_error the following option should be used
cpa.arg.witness.removeInsufficientEdges=false
- Status changed from Open to Resolved
Added the proposed option and several fixes in ET parser to deal with new obtained witnesses. Seems that all work fine.
- Status changed from Resolved to Closed
I merged the branch to master in 28c3b5a8.
Also available in: Atom
PDF