Klever

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.

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.