Feature #8494: Process extended format of violation witnesses
Get rid of temporary variables and their removing
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.
Updated by Evgeny Novikov about 1 year ago
- Status changed from Resolved to Closed
- File Screenshot_20200120_184150.png Screenshot_20200120_184150.png added
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.