Termination analysis gives up for loops with multiple conditions

[leunam99]

I came across the following (slightly adapted) program from sv-comp:

int main() {
    int c, x, y;
    c = 0;
    if (y > 46340) return 0;
    while ((x > 1) && (x < y)) {
        x = x*x;
        c = c + 1;
    }
    return 0;
}

When checking the termination property, I get a warning: The program might not terminate! (Upjumping Goto). Looking at the cil version of the program I get

int main(void) 
{ 
  int c ;
  int x ;
  int y ;

  {
#line 9
  c = 0;
#line 10
  if (y > 46340) {
#line 10
    return (0);
  }
  {
#line 11
  while (1) {
    while_continue: /* CIL Label */ ;
#line 11
    if (x > 1) {
#line 11
      if (! (x < y)) {
#line 11
        goto _L;
      }
    } else {
      _L: /* CIL Label */ 
#line 11
      goto while_break;
    }
#line 12
    x *= x;
#line 13
    c ++;
  }
  while_break: /* CIL Label */ ;
  }
#line 15
  return (0);
}
}

If I remove the #line pragmas from this, the termination analysis succeeds. The problem seems to be that the termination analysis compares the location of the goto and the label to exclude loops, but because the locations take these line numbers into account, they do not represent the actual relation of the code.

[sim642]

The upjumping check being bad is a known issue from the start (#1245), but we can keep this open because it shows other implications to more complex loops.