Project

General

Profile

Feature #8897

Update CPAchecker

Added by Evgeny Novikov about 1 year ago. Updated about 1 year ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Addons
Target version:
Start date:
05/28/2018
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

Ilja already has some recent experience in this, so, let's him allow to do this in production.

History

#1

Updated by Ilja Zakharov about 1 year 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.

#2

Updated by Evgeny Novikov about 1 year 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.

#3

Updated by Ilja Zakharov about 1 year 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).

#4

Updated by Vadim Mutilin about 1 year 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

#5

Updated by Ilja Zakharov about 1 year 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.

#6

Updated by Evgeny Novikov about 1 year ago

  • Status changed from Resolved to Closed

I merged the branch to master in 28c3b5a8.

Also available in: Atom PDF