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!