Feature #10550

Feature #8119: Develop preset tags

Develop preset tags for CPAchecker BAM

Added by Evgeny Novikov 3 months ago. Updated about 1 month ago.

Preset jobs, marks and tags
Target version:
Start date:
Due date:
% Done:


Estimated time:
Published in build:


CPAchecker BAM reports false alarms either due to specific configuration options used for optimization purposes or due to some internal inaccuracies. As a result of this feature request I expect a subtree of corresponding tags with appropriate descriptions in any suitable form.



Updated by Pavel Andrianov 3 months ago

  • Predicate Analysis (Problems with predicate CPA)
    • Arrays (Predicate analysis considers only the first element by default in uf encoding)
    • Unallocated memory (Predicate analysis considers initialized, but unallocated memory as having any value)
    • Dynamic structures (Predicate analysis have certain troubles considering lists and other dynamic structures)
    • mem-functions (Memset, memcpy, and so on are not completely supported)
    • Bit precise (There are bit operations which are not completely supported by defult)
  • Function Pointer Analysis (Problems with FunctionPointerCPA)
  • BAM (Problems with BAM CPA)
  • Value analysis (Problems with ValueCPA)
  • Assembler code (Verifier does not consider assembler code)

I may miss some cases, as I did not mark sequential launches long ago. Thus, better that someone takes a look.


Updated by Evgeny Novikov about 1 month ago

  • Status changed from New to Resolved

I added these tags to preset ones in branch bridge_9396.


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

Also available in: Atom PDF