Project

General

Profile

Feature #8083

Add tests for static verification tools

Added by Evgeny Novikov over 2 years ago. Updated over 1 year ago.

Status:
Closed
Priority:
Urgent
Category:
Testing
Target version:
Start date:
04/18/2017
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

We know that CPAchecker has quite many assumptions that can result in strange verification results. For instance, it does not track array elements except the first one. Tests should explicitly demonstrate this. Likely here is the most important and often annoying assumptions:
  1. Memory tracking (if there isn't memory allocation or it is too complicated then CPAchecker does not track it).
  2. Arrays tracking.
  3. Function pointer assumptions (nothing is called if function pointer is unknown).
  4. Bitwise support (by default it is not performed yet).
  5. Ignoring assembly code (sometimes that hits).

Note that specific rules like generic:memory and sync:race have a lot of other assumptions - corresponding tests are also welcome.

History

#1

Updated by Evgeny Novikov over 2 years ago

  • Description updated (diff)
#2

Updated by Evgeny Novikov almost 2 years ago

  • Target version set to 1.0
#3

Updated by Evgeny Novikov almost 2 years ago

  • Subject changed from Add tests for CPAchecker to Add tests for static verification tools
  • Status changed from New to Resolved

I did it in faba1ac6 to branch tests.

#4

Updated by Evgeny Novikov over 1 year ago

  • Status changed from Resolved to Closed

I merged branch tests to master in f96d83aa.

Also available in: Atom PDF