Feature #8083
Updated by Evgeny Novikov over 7 years ago
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:
# Memory tracking (if there isn't memory allocation or it is too complicated then CPAchecker does not track it).
# Arrays tracking.
# Function pointer assumptions (nothing is called if function pointer is unknown).
# Bitwise support (by default it is not performed yet).
# 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.