better regression testing

Problems with the current solution (update_suite.rb):

• setup: dependency on ruby and gem install parallel
• another programming language for beginners
• the code is hard to understand
• argument parsing is very manual, only fixed order works
• regtest.sh (which allows passing extra arguments for debugging individual cases) should be combined
• it's not very fast
  • with dune runtest it could only re-run only things that changed (also it could keep preprocessed input, syntax-highlighted source etc.)
• it's not very flexible
  • if we do checks in goblint, we could better handle precision changes
• we use comments to check results:
  https://github.com/goblint/analyzer/blob/6ebe8168c19687c6227ac41127f1e7c02a46e4d9/scripts/update_suite.rb#L385-L386

Original comment for this issue was regarding the last point.

@jerhard and I were tossing this back and forth over lunch and something we discussed at some point was using something along the lines of __goblint_check(a == 42, __GOBLINT_UNKNOWN) or __goblint_check(x ==17, __GOBLINT_SUCCESS) in the regression tests instead of having an assert(...) //UNKNOWN.

Then, the expected result is immediately obvious to Goblint itself, and Goblint can either output things for all asserts or only those where something failed without having to somehow do a regex on the comments.

Also, once could use the syntactic search to identify those places where __goblint_check(...) is called that are unreachable and then also warn there that the assert is unreachable. (These are the cases where warnings are missing in ./regtest.sh vs the ruby script).

The question that is still open is how to integrate warnings different from asserts into this setting.

Opinions?

Originally posted by @michael-schwarz in https://github.com/goblint/analyzer/issues/286#issuecomment-879796205

Start by reading scripts/update_suite.rb and regtest.sh to understand the current regression-test workflow, argument handling, and comment-based result checks. Review the proposed __goblint_check assertions in the issue and determine how warnings different from assertions should be represented. Done means an agreed, integrated replacement that supports the stated test and debugging workflows.