Changes for Pull Request bench#85: Automatic Generation of Test Cases for Incremental Static Analysis

[J2000A]

Changes needed for the "Test Automation for Incremental Analysis - TAIA" from the pull request in the bench repository:

• Add new goblint check annotation NOFAIL which expresses the knowledge the incremental analysis should have: After an incremental analysis the check should either be successful or unknown, but not fail. The TODO annotation is similar but not sufficient, as the update_suite.rb script ignores these annotations.

• Add new goblint check annotation NOTINPRECISE which checks that the incremental analysis did not get less precise. After an incremental analysis the check should either be successful or failing, but not unknown. Failing tests are ignored to only warn in case if inprecision, as we intend to check only for the precision and not the correctness.

• Add a reference to the "Test Automation for Incremental Analysis - TAIA" in the documentation.

• Improve the regex in the update_suite.rb script for matching annotations. The annotations are sometimes part of code generated by cil (e.g. SOME_CIL_VARIABLE_FAIL). To prevent false matchings the annotation should start with a word boundary \b or a / for the case that the annotation was written directly after a comment (e.g. //SUCCESS).

• When there is an exception in the update_suite.rb print the content of the warn-file for easier debugging.

• In the update_suite.rb script use the // PARAM: string at the first line also for the incremental tests.

• Add a bool option trans.goblint-check for writing out __goblint_check()s instead of __VERIFIER_asserts.

• Change the depreciated parameter --sets in the regression test 46/26 to --set

• Change MAYFAIL to MAY FAIL for regression test 36/86, 58/15 and 67/16. Otherwise the FAIL would not be recognized by the tester due to the changed regex matching of the annoations.