Project

General

Profile

Actions

Feature #10754

closed

Update CPAchecker (SMG)

Added by Evgeny Novikov 10 months ago. Updated 7 months ago.

Status:
Closed
Priority:
Urgent
Category:
Addons
Target version:
Start date:
03/13/2021
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

We expect that CPAchecker (SMG) will improve representation of verification results (violation witnesses and code coverage). This will facilitate users especially newcomers. Also, bug fixes and optimizations are always welcome.


Related issues

Blocks Klever - Feature #10794: Add notes from CPAchecker SMG to code coverageClosedEvgeny Novikov04/07/2021

Actions
Actions #1

Updated by Evgeny Novikov 10 months ago

  • Blocks Feature #10794: Add notes from CPAchecker SMG to code coverage added
Actions #2

Updated by Evgeny Novikov 10 months ago

  • Priority changed from High to Urgent

We will need to update CPAchecker (SMG) to get highly demanded improvements in representation of witnesses and code coverage.

Actions #3

Updated by Evgeny Novikov 9 months ago

Temporarily I updated CPAchecker to https://github.com/Druidos/cpachecker/commit/953c051 in branch update-cpachecker. Most likely there will be further updates that in particular will be in the primary SVN repository rather than in the GitHub mirror.

Actions #4

Updated by Evgeny Novikov 8 months ago

  • Assignee changed from Anton Vasilyev to Evgeny Novikov

The branch was merged to branch coverage-notes and then to better-code-coverage. In the latter branch I switched CPAchecker back to branch klever_fixes where Anton moved all changes made in his own repository.

Actions #5

Updated by Evgeny Novikov 7 months ago

  • Status changed from New to Resolved

I updated CPAchecker to klever_fixes:37649 in branch better-code-coverage, so, now CPAchecker provides awesome verification results. Let's see on CI results.

Actions #6

Updated by Evgeny Novikov 7 months ago

  • Status changed from Resolved to Closed

Tests passed, so, I merged the branch to master in d17402872. So, now all users will have a greatly improved representation of violation witness and code coverage when using CPAchecker SMG for checking memory safety.

Actions

Also available in: Atom PDF