Skip to content

replace __VERIFIER_error by empty implementation

🤖 SoSy-Bot 🤖 requested to merge verifier_error_implementation into master

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:

  1. 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_*
  2. 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 function panic. It was causing a build error because panic was just calling __VERIFIER_error and __VERIFIER_error was annotated with __noreturn__ previously
  3. 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 used reach_error and not reach_error();abort();
  4. 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)

Merge request reports