Package de.uka.ilkd.key.speclang.njml

Failed tests

• ContractLoadingTests. issues1658()
• ContractLoadingTests. specMathBigintMathTest()
• ContractLoadingTests. specMathJavaMathTest()
• ContractLoadingTests. sumAndMax()
• ExpressionTranslatorTest. [10] (\infinite_union int i; \nothing)
• ExpressionTranslatorTest. [11] 1.f < 2.f < 3.f
• ExpressionTranslatorTest. [12] 1.f + 2.f
• ExpressionTranslatorTest. [13] 1. + 2
• ExpressionTranslatorTest. [14] 1f + 2d
• ExpressionTranslatorTest. [1] 1+1
• ExpressionTranslatorTest. [2] 1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1+1
• ExpressionTranslatorTest. [3] \result
• ExpressionTranslatorTest. [4] this
• ExpressionTranslatorTest. [5] (\forall int i; i + i == 2)
• ExpressionTranslatorTest. [6] (\exists int i; i%2 == 2)
• ExpressionTranslatorTest. [7] (\exists int i; 0 < i < 2; i%2 == 2)
• ExpressionTranslatorTest. [8] 1 < 2 < 1+1+1
• ExpressionTranslatorTest. [9] 1+2*3
• NJmlTranslatorTests. testContractModifiers()
• NJmlTranslatorTests. testContractModifiersMultiple()
• NJmlTranslatorTests. testContractModifiersMultipleAlso()
• NJmlTranslatorTests. testIgnoreOpenJML()
• NJmlTranslatorTests. testWarnRequires()

Classes