Feature #9825
closedFeature #8494: Process extended format of violation witnesses
Get rid of temporary variables and their removing
0%
Description
Like with auxiliary functions, several components (namely CIL and CPAchecker) can produce temporary variables that will be referred within violation witnesses and thus error traces. We tried to remove some of these variables if this can be done rather safely, but corresponding code is very complicated and buggy.
I suggest to get rid of as many temporary variables as possible (for CIL we will need to fix it or to turn on some options, for CPAchecker as well as all other verifiers we will need to use source file references for showing source code in error traces) and then we will be able to get rid of temporary variables removing code in Core VRP.
Files
Updated by Evgeny Novikov about 5 years ago
- Blocks Feature #9897: Develop tutorial added
Updated by Evgeny Novikov about 5 years ago
- Blocks deleted (Feature #9897: Develop tutorial)
Updated by Evgeny Novikov almost 5 years ago
- Blocked by Feature #9985: Fold temporary variables back added
Updated by Evgeny Novikov almost 5 years ago
For CPAchecker the suggested thing is in master already. Please, test it as soon as possible.
Updated by Evgeny Novikov almost 5 years ago
- Blocked by Feature #9906: Update CIL added
Updated by Evgeny Novikov almost 5 years ago
- Category set to Results processing
- Status changed from New to Resolved
I did this in branch no-tmp-vars. Wait for test results.
Updated by Evgeny Novikov almost 5 years ago
- File Screenshot_20200120_184150.png Screenshot_20200120_184150.png added
- Status changed from Resolved to Closed
There is no any regressions, so I merged the branch to master in 3346c2236. Until we will update CPAchecker and switch to extended violation witnesses eventually one will see non-pretty pieces of code for if statements like selected at the following screenshot.