Project

General

Profile

Actions

Feature #10998

closed

Update CPAchecker SMG

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

Status:
Closed
Priority:
High
Category:
Addons
Target version:
Start date:
10/29/2021
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

We are using CPAchecker SMG that is more actual than in trunk, but we expect that Anton will eventually merge his branch into trunk, so we will be able to switch back to trunk one day.

Actions #1

Updated by Evgeny Novikov about 1 year ago

I updated CPAchecker to klever_fixes:38771 in branch update_cpachecker. There were some regressions, but eventually I merged the branch to master in eb0fdae13. This update does not make all things that are necessary by this feature, so let's update CPAchecker later one more time.

Actions #2

Updated by Evgeny Novikov about 1 year ago

One more update of CPAchecker to klever_fixes:38949 was made in branch update-cpachecker. After tests passed, I merged this branch to master in 7189947cf. Now, when one will use verifier profile "memory checking without uncertainty", he/she will get error traces that consider undefined functions as errors. CPAchecker provides exact places and paths to those undefined functions that simplifies debugging.

Actions #3

Updated by Evgeny Novikov 12 months ago

In ce804b7 to master CPAchecker was updated to klever_fixes:39071. In this version Anton fixed work with assignments of structures that in particular should improve finding undefined functions.

Actions #4

Updated by Evgeny Novikov 9 months ago

  • Status changed from New to Closed

Anton transferred most changes from his development branch to trunk, but there is still some work to do. It can take pretty much time to finish that work, so let's include an appropriate update to Klever 3.5.

Actions

Also available in: Atom PDF