problem in CBMC/Java coverage analysis without `LineNumberTable`

[mgudemann]

for the following program

class simple
{
  int f(int a, int b)
  {
    if(a < b)
      return a;
    else
      return b;
  }
}

reports 0 out of 0 covered goals (--cover location) when the class file is compiled using -g:vars which creates a LocalVariableTable but no LineNumberTable attribute.
Without this compilation switch or with full debugginf information using -g, CBMC reports 3 out of 4 covered goals. The GOTO function is created correctly in any case, lack of line number information seems to prevent generation of coverage ASSERTs.

[peterschrammel]

obsolete