Feature #10883
closedSupport ldv_assert() for memory safety
0%
Description
It turned out that in some cases it is better to express violations of various requirements as violations of memory safety properties, e.g. as null pointer dereference. Let's use the same API, i.e. ldv_assert(), but different implementations of it depending on properties being checked.
Updated by Evgeny Novikov almost 3 years ago
- Status changed from New to Resolved
I implemented this feature in branch ldv-assert-for-memory-safety. A useful hint for everybody is that you can invoke ldv_assert() somewhere in your program sources that is often used for debugging. Both for CPAchecker SMG and CPAchecker BAM (i.e. when you check memory safety and reachability correspondingly) it will result to an immediate bug automatically and unconditionally, of course if the verification tool will prove that it is reachable.
Updated by Evgeny Novikov almost 3 years ago
- Status changed from Resolved to Closed
After CI failed I realized that it is not correct to develop common models that depend on macro conditions. After all I decided to completely get rid of common model "verifier/common.c" and thus definition of function "ldv_assert()". Now "ldv_assert()" is a macro for both memory safety and reachability. Unfortunately, this change will cause new verification results will not be automatically assessed well with existing expert marks (there is one more function call in their error trace patterns), but this inconvenience will disappear rather soon.
After all CI passed, so, I merged the branch to master in 9892b743c.
One more time, now you can insert "ldv_assert()" anywhere in target source code independently on checked properties. This will cause a verification tool to report an unsafe, if it will prove that this location is reachable. This doesn't work for concurrency checking as it has another mechanism for detecting bugs.