Expression locations for parts of `for` loop are sometimes wrong

[sim642]

Increment part has (offset) initializer location

    for (int *p = NULL; 1; (*p)++) {}

Actual Goblint warning is

[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (bar.c:5:14-5:22)
      for (int *p = NULL; 1; (*p)++) {}
               ^^^^^^^^

Expected Goblint warning would be

[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (bar.c:5:28-5:34)
      for (int *p = NULL; 1; (*p)++) {}
                             ^^^^^^

Increment part has (offset) entire location

    int *p;
    for (p = NULL; 1; (*p)++) {}

Actual Goblint warning is

[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (bar.c:8:9-8:28)
      for (p = NULL; 1; (*p)++) {}
          ^^^^^^^^^^^^^^^^^^^

Expected Goblint warning would be

[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (bar.c:8:23-8:29)
      for (p = NULL; 1; (*p)++) {}
                        ^^^^^^

Condition part has (offset) entire location

    for (int *p = NULL; (*p)++; (*p)++) {}

Actual Goblint warning (in addition to above) is

[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (bar.c:6:9-6:38)
      for (int *p = NULL; (*p)++; (*p)++) {}
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Expected Goblint warning would be

[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (bar.c:6:25-6:31)
      for (int *p = NULL; (*p)++; (*p)++) {}
                          ^^^^^^

[michael-schwarz]

Do you have an example so this issue is complete and can be tackled also by others? Or do you intend to do it yourself soon?

[sim642]

I'll add some examples soon (they're very simple), I just created the issue during a conversation to not forget.

EDIT: I added three to the original description now.
By the way, the columns being offset is not just a general off-by-one error. They are correct in other simpler situations, for example:

    int *p = NULL;
    return *p;

Actual and expected Goblint warning is

[Error][Behavior > Undefined > NullPointerDereference][CWE-476] Must dereference NULL pointer (bar.c:10:12-10:14)
      return *p;
             ^^

[sim642]

#211 fixes the biggest issues here. The offset parts are extracted to #213 and #214.