goblint / cil

C Intermediate Language
https://goblint.github.io/cil/
Other
130 stars 19 forks source link

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

Open sim642 opened 2 hours ago

sim642 commented 2 hours ago

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 commented 2 hours ago

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