Feature #9825

Feature #8494: Process extended format of violation witnesses

Get rid of temporary variables and their removing

Added by Evgeny Novikov 10 months ago. Updated 6 months ago.

Results processing
Target version:
Start date:
Due date:
% Done:


Estimated time:
Published in build:


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.


Screenshot_20200120_184150.png (11.8 KB) Screenshot_20200120_184150.png Evgeny Novikov, 01/20/2020 06:42 PM

Related issues

Blocked by Deductive Verification Tools for Linux Kernel - Feature #9985: Fold temporary variables backClosed12/13/2019

Blocked by Klever - Feature #9906: Update CILClosed11/08/2019




Updated by Evgeny Novikov 8 months ago


Updated by Evgeny Novikov 8 months ago


Updated by Evgeny Novikov 7 months ago


Updated by Evgeny Novikov 7 months ago

For CPAchecker the suggested thing is in master already. Please, test it as soon as possible.


Updated by Evgeny Novikov 6 months ago


Updated by Evgeny Novikov 6 months ago

  • Status changed from New to Resolved
  • Category set to Results processing

I did this in branch no-tmp-vars. Wait for test results.


Updated by Evgeny Novikov 6 months ago

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.

Also available in: Atom PDF