Seemingly incorrect definite assignedness after true/false
Issue #89
resolved
The equations for definite assignedness after true/false seem incorrect when comparing to the specification in JLSv3 16.1.7:
Actually, the definite assignedness after true/false checks look incorrect. Diff against what they probably should be:
 eq Expr.isDAafterFalse(Variable v) = isTrue()  isDAbefore(v);  eq Expr.isDAafterTrue(Variable v) = isFalse()  isDAbefore(v); + eq Expr.isDAafterFalse(Variable v) = isTrue()  isDAafter(v); + eq Expr.isDAafterTrue(Variable v) = isFalse()  isDAafter(v);
This is difficult to find a test case to check, and applying the patch above causes lots of regressions.
Comments (4)

reporter 
reporter Test errors caused by stack overflows. Some incorrect circular evaluation in the DAafterFalse attribute.

reporter The problem was an additional error in
Expr.isDAafter
: eq Expr.isDAafter(Variable v) = (isDAafterFalse(v) && isDAafterTrue(v))  isDAbefore(v); + eq Expr.isDAafter(Variable v) = isDAbefore(v);
This caused for example integer literals to incite an infinite recursive call chain.

reporter  changed status to resolved
 Log in to comment
There are equations for
Binary
which provide the correct value in most cases,however
CastExpr
is a subtype ofExpr
but notBinary
so it is not covered by the correct expressions so I was able to create a test case using this info:This case finally exposes a bug in the equations. However, the question is why I get regressions when I apply the fix.