CI considers [Info] messages to be a violation of //NOWARN

[michael-schwarz]

In the course of #1094, we discovered that our CI considers messages such as the following to be a violation of the //NOWARN annotation.

[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (05-oob-implicit-deref.c:10:4-10:35)

Normally, the solution might be to not write such annotations, but the problem is that such issues may, e.g., arise from a high fortification level, turning

// This     
memset(ptr, 0, four * sizeof(int)); //NOWARN 

// into this
size_t  tmp = __builtin_object_size(ptr, 0); //NOWARN
__builtin___memset_chk(ptr, 0, four * sizeof(int), tmp); //NOWARN

where with //NOWARN we want to check the absence of some actual warning rather than some internal.

My proposed solution would be to not consider messages of the severity Info as violations of the //NOWARN annotation. Warnings should be given to the user with a higher severity anyway.

[sim642]

At some point this was required because // WARN doesn't allow more precise matching.

This on its own won't really fix the issues with fortification though. There's #706 about it. The trouble is that with fortification some warnings move to header files where our comment annotations no longer check them correctly.

[michael-schwarz]

Yes, it won't fix the fortification issue in general, but it would fix this specific issue.

[sim642]

These are the test failures for // WARN when changing this:

Expected warn, but registered other on assume-unknown:16
  __goblint_assume_join(id2); // WARN joining unknown thread ID, make joined set All threads
Expected warn, but registered other on assume-unknown:20
  pthread_create(&id, NULL, t_fun, NULL); // WARN make joined set different from All threads
51/05 failed!

Expected warn, but registered other on mixedjmpbufs:12
    longjmp(error1, 1); // WARN (modified since setjmp)
Expected warn, but registered other on mixedjmpbufs:20
    longjmp(error0, 1); // WARN (modified since setjmp)
68/31 failed!

Expected warn, but registered other on munge:41
      longjmp(buf1, 1); //WARN
68/33 failed!

3 test(s) failed: ["51/05 assume-unknown", "68/31 mixedjmpbufs", "68/33 munge"]

For // NOWARN there's no good way to know where it might be tested for.

[michael-schwarz]

The question is whether some other message is simply hiding a bug here... We should produce actual warnings in those cases and not just some random info messages....