replace __VERIFIER_error by empty implementation
Created by: skanav
This pull request replaces __VERIFIER_error
with empty implementation. A new function reach_error
is created and all the calles to __VERIFIER_error
are replaced by reach_error();abort();
.
The following points are still to be addressed:
- In the folder
eca-rers2018
there are many similar functions with the name of the format__VERIFIER_error_XX
where XX is an integer from 0 to 99. At the moment I have kept them as they were. There is an unreach call property for each of these functions. I think they should also be replaced, but we can deal it in a separate PR too. One could say that only__VERIFIER_error
was part of the rules, not__VERIFIER_error_*
- In the folder
òpenbsd-6.2
the build failed after the changes by the script. I had to change a few preprocessed files and a header file manually to remove the tag__noreturn__
from the functionpanic
. It was causing a build error because panic was just calling__VERIFIER_error
and__VERIFIER_error
was annotated with__noreturn__
previously - In a few cases
__VERIFIER_error
is used inside a tertiary operator, e.g.cond ? __VERIFIER_error() : (void)0
. In these cases I have just usedreach_error
and notreach_error();abort();
- If we grep for
__VERIFIER_error_
we still see a lot of functions. I have kept them as they were. They are not part of the sv-comp rule. I assumed that only__VERIFIER_error
was part of the rules, not__VERIFIER_error_*
closes #655 (closed)