Spurious Warning: Body of function ... falls-through and cannot find an appropriate return value

[michael-schwarz]

Sometimes, particularly when dealing with code that CIL produced from code that contained a switch, we produce spurious warnings Warning: Body of function test falls-through and cannot find an appropriate return value.

E.g.

typedef struct s_0 {int a;} s;

s test(int param) {
    s one;
    switch(param) {
        case 3:
            one = (s){7};
            return one;
        default:
            one = (s){7};
            return one;
    }
}

int main() {
    test(7);
}

CIL transforms this into:

s test(int param ) 
{ 
  s one ;
  s __constr_expr_0 ;
  s __constr_expr_1 ;

  {
  {
  if (param == 3) {
    goto case_3;
  }
  goto switch_default;
  case_3: /* CIL Label */ 
  __constr_expr_0.a = 7;
  one = __constr_expr_0;
  return (one);
  switch_default: /* CIL Label */ 
  __constr_expr_1.a = 7;
  one = __constr_expr_1;
  return (one);
  switch_break: /* CIL Label */ ;
  }
}

When running CIL again on the CILed program we get the spurious warning.

This is a low priority issue discovered during goblint/bench#16 and I opened it mostly such that we can refer to it when we see this error message.