Support __noreturn__ or a selection of non-returning functions
Currently, we do not support the common GNU C attribute __noreturn__
. Because of this, for example calls to abort()
are treated by CPAchecker like casual functions that return.
Unless there already is a way to change this, we could think about supporting either the __noreturn__
attribute directly (if Eclipse parser supports it), or use a configurable list of non-returning function calls.
Maybe it is also important for termination analysis, whether __noreturn__
should be treated as 'runs forever' instead of 'terminates'.