search

delcypher / freeboogie

Automatically exported from code.google.com/p/freeboogie
0 stars 1 forks source link

display warnings once #59

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
Warnings such as "Command is unreachable" appear after each typecheck, so
the user sees them about 8 times.

Original issue reported on code.google.com by radugrig...@gmail.com on 18 Sep 2009 at 1:11

GoogleCodeExporter commented 9 years ago 
In fact, unreachable commands may be introduced by transformers, and they 
shouldn't
be reported. For example:
  if (*) {
    goto X;
  }
  X: ...
becomes
  goto A, B;
  A: goto X;
  goto C; // unreachable
  B: goto C;
  C: assume true;
  X: ...
simply because the IfDesugarer does not analyze the content of the 'yes' branch 
to
see that the latest statement is a goto. This seems reasonable. On the other 
hand,
introducing unreachable commands is often a bug (that was the case, for 
example, wit
introducing copy commands). So I need to be careful.

Original comment by radugrig...@gmail.com on 18 Sep 2009 at 2:19