Feature #10998
closed
Added by Evgeny Novikov over 2 years ago.
Updated about 2 years ago.
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.
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.
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.
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.
- 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.
Also available in: Atom
PDF