Project

General

Profile

Actions

Feature #9825

closed

Feature #8494: Process extended format of violation witnesses

Get rid of temporary variables and their removing

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

Status:
Closed
Priority:
Urgent
Category:
Results processing
Target version:
Start date:
09/18/2019
Due date:
% Done:

0%

Estimated time:
Published in build:

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

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

Related issues 2 (0 open2 closed)

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

Actions
Blocked by Klever - Feature #9906: Update CILClosedEvgeny Novikov11/08/2019

Actions
Actions #1

Updated by Evgeny Novikov over 4 years ago

Actions #2

Updated by Evgeny Novikov over 4 years ago

Actions #3

Updated by Evgeny Novikov over 4 years ago

Actions #4

Updated by Evgeny Novikov over 4 years ago

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

Actions #5

Updated by Evgeny Novikov about 4 years ago

Actions #6

Updated by Evgeny Novikov about 4 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.

Actions #7

Updated by Evgeny Novikov about 4 years 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.

Actions

Also available in: Atom PDF