Analyzing a real-world C project, we could extract the following minimized example:

int sprnames[3] = {
    1,2,3
};

int main(int argc, char const *argv[])
{
    int* namelist;
    namelist = sprnames;
    while (*namelist != 0)
	    namelist++; 
    
    return 0;
}

Of course, the program over-confidently relies on the 4th cell of the array to be zero. This is afaik not guaranteed. The pattern, as brittle as it is seems to be a common one of programs of this era. Goblint flags this as dead after the loop:

[Warning][Deadcode] Function 'main' does not return
[Warning][Deadcode] Function 'main' has dead code:
  on line 13 (evil.c:13-13)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 4
  dead: 1
  total lines: 5
[Warning][Deadcode][CWE-571] condition '*namelist != 0' (possibly inserted by CIL) is always true (evil.c:10:12-10:26)

Would we not rather want to consider the loop condition unknown in the end, and continue with the rest alive?