Skip to content

Opt out of Termination-{MainControlFlow, BitVector} and Concurrency-Memsafety Subcategory

Henrik Wachowitz requested to merge cpachecker-validator-opt-out into main

CPAchecker opts out of the following subcategories:

Termination BitVector & Termination MainControlFlow

Both categories require non-linear arithmetic (nla). CPAchecker's termination analysis is based on LassoRanker and does not support nla. Thus, we are unable to handle and confirm witnesses in these categories.

Concurrency-Memsafety

We use BDDs as abstract domain for concurrent programs. This analysis does not handle heap memory soundly and is thus unsuited for witness validation in this category.

Edited by Henrik Wachowitz

Merge request reports