`do`-`while` loop `continue` label incorrect

[sim642]

A simple do-while loop like

  do {
    i++;
  } while (i < 10);

is converted to the following (according to Goblint's justcil):

  {
#line 6
  while (1) {
    while_continue: /* CIL Label */ ;
#line 7
    i ++;
#line 6
    if (! (i < 10)) {
#line 6
      goto while_break;
    }
  }
  while_break: /* CIL Label */ ;
  }

The location of while_continue label there is wrong! According to cppreference, it should be like:

do {
    // ... 
    continue; // acts as goto contin;
    // ... 
    contin:;
} while (/* ... */);

[michael-schwarz]

Wow! Amazing this was only discovered after almost 2 decades of CIL!

[michael-schwarz]

I tried to reproduce this, but there does not seem to be a problem. A continue in the loop does not jump to this while_continue label, but to a label __Cont introduced by CIL.

  int i = 0;
  int k = 0;

  do {
    i++;
    if(i == 1) { continue; }
    k = 8;
  } while ( i < 1);

turns into

  int i ;
  int k ;

  {

  i = 0;

  k = 0;

  while (1) {

    i ++;

    if (i == 1) {

      goto __Cont;
    }

    k = 8;
    __Cont: /* CIL Label */ 

    if (! (i < 1)) {
      break;
    }
  }

If there is any miscompilation observable in Goblint, it seems like it's an issue with Goblint transformations, and a issue should be opened there.

Feel free to re-open if there is an actual CIL issue!

[sim642]

Oh, interesting!

What's the while_continue label for then, if not continue?

Perhaps it makes sense to rename it or remove it altogether (if it's not needed), because this is just confusing.