Polish `__goblint_check`

[sim642]

In #278 all the asserts in tests were changed to __goblint_check, which is declared by a goblint.h header that we forcefully include into every analyzed file via -include. This makes the programs normally uncompilable and most of them still include assert.h, which now is excessive.

This situation should be improved:

• Add explicit #include <goblint.h> to all tests using __goblint_check.

• Remove excessive #include <assert.h> from such tests.

• Add explicit #include <goblint.h> to all tests using __goblint_assume_join, __goblint_split_begin and __goblint_split_end.

• Provide a dummy implementation for goblint.h, which wouldn't be used for analysis (they're handled as specials), but could be used for compiling the programs. It would also allow using Goblint function annotations in actual projects/stories.

• Document __goblint_check, etc as function annotations like __goblint_assume_join is documented in Interactive: improvements for chrony story #724.

• Design a better structure for our includes directory: right now it contains a mix of various things and cannot be added to include paths of actual projects:

  1. Goblint-specific headers: goblint.h, linux/goblint_preconf.h, linuxlight.h?
  2. Goblint overrides of standard headers: assert.h.
  3. Goblint stubs for standard functions: stdlib.c, pthread.c.
  4. Goblint stubs for non-standard functions: sv-comp.c.
  5. And eventually general stubs for Goblint-specific functions: goblint.c.

  They should be split by these various types. Moreover, each of them should have standard structure (include, src, etc).

• Rename includes to something better since it also contains various stub implementations.