Project

General

Profile

Actions
Copy link

Feature #10549

closed

Feature #8119: Develop preset tags

Develop preset tags for CPAchecker SMG

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

Status:
Closed
Priority:
Urgent
Assignee:
Anton Vasilyev
Category:
Preset jobs, marks and tags
Target version:
3.0
Start date:
10/21/2020
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

CPAchecker SMG has many tricky reasons of false alarms. As a result of this feature request I expect a subtree of corresponding tags with appropriate descriptions in any suitable form.

Actions
Copy link
 #1

Updated by Anton Vasilyev about 4 years ago

  • String library (Unsupported functions like strlen, strcpy)
  • PredicateSMG
    • Arithmetics (Arithmetics and assignments of nonexplicit values produces unknown symbolic value, which could result in false overflow report)
  • SMG
    • Packed/alligned (Wrong size calculation of packed/alligned structures)
    • Abstraction (Incorrect memleak report of abstracted list segments)
    • Dynamic allocation (If analysis cannot calculates explicit size for allocation, it assumes that size is 3 byte)
Actions
Copy link
 #2

Updated by Evgeny Novikov about 4 years ago

  • Status changed from New to Resolved

I added these tags to preset ones in branch bridge_9396.

Actions
Copy link
 #3

Updated by Evgeny Novikov about 4 years ago

  • Status changed from Resolved to Closed

I merged this branch to master in 2625e7311 after CI passed test cases. This change is not backward compatible. Moreover, you should migrate your marks manually using preset tags as most as possible.

Actions
Copy link

Also available in: Atom PDF