Feature #8897
closedUpdate CPAchecker
0%
Description
Ilja already has some recent experience in this, so, let's him allow to do this in production.
Updated by Ilja Zakharov over 6 years ago
- Status changed from New to Resolved
Implemented in 8897-trunk-cpachecker. Updated CPAchecker in Klever for SMG and reachability up to 27946 of trunk.
Updated by Evgeny Novikov over 6 years ago
- 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.
Updated by Ilja Zakharov over 6 years ago
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).
Updated by Vadim Mutilin over 6 years ago
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
Updated by Ilja Zakharov over 6 years ago
- 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.
Updated by Evgeny Novikov over 6 years ago
- Status changed from Resolved to Closed
I merged the branch to master in 28c3b5a8.