Does not detect that a method's exceptional behavior should throw an exception.

[Rafael-Baltazar]

JMLCUTE does not detect that the method add(int, int) (below) should throw an exception, given x = 0 and y = 0.

Class under test:

public class LinearArithmetic {
  /*@
   @  requires x > 0 && y > 0;
   @  assignable \nothing;
   @  ensures \result == \old(x) + \old(y);
   @ also
   @  requires x <= 0 || y <= 0;
   @  assignable \nothing;
   @  signals(Exception) true;
   */
  public int add(int x, int y) throws Exception {
    return x + y;
  }
}

Simplified generated advice:

int result = 0;
final int old0 = x;
final int old1 = y;
try {
  result = proceed(receiver, x, y);
  cute.Cute.Assert(result == old0 + old1);
} catch (Throwable e) {
  if ((x > 0) && (y > 0)) {
    cute.Cute.Assert(e instanceof Exception || e instanceof RuntimeException);
  }
  if ((x <= 0) || (y <= 0)) {
    cute.Cute.Assert(true);
  }
}
return result;

Giving x = 0 and y = 0, the advice executes the normal flow, without executing catch block.