Project

General

Profile

Actions
Copy link

Feature #10998

closed

Update CPAchecker SMG

Added by Evgeny Novikov over 2 years ago. Updated about 2 years ago.

Status:
Closed
Priority:
High
Assignee:
Evgeny Novikov
Category:
Addons
Target version:
3.4
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
Copy link
 #1

Updated by Evgeny Novikov over 2 years 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
Copy link
 #2

Updated by Evgeny Novikov over 2 years 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
Copy link
 #3

Updated by Evgeny Novikov over 2 years 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
Copy link
 #4

Updated by Evgeny Novikov about 2 years 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
Copy link

Also available in: Atom PDF