Test Summary
|
25%
successful |
Failed tests
- Gradle Test Executor 1. failed to execute tests
- TestContextStatementBlock. testContextTermInstantiation()
- TestJP2KeY. initializationError
- TestJP2KeY. initializationError
- TestJP2KeY. testReadBlockWithContext()
- TestJavaCardDLJavaExtensions. testMethodFrameRedirectsScope()
- TestJavaInfo. initializationError
- TestDeclarationProgramVariableCollector. testVisitor()
- LabeledTermImplTest. testEqualsLabelOnTop()
- LabeledTermImplTest. testGetHasAndContainsLabels()
- TestClashFreeSubst. testClash()
- TestClashFreeSubst. testClashInSubstTerm()
- TestClashFreeSubst. testMultiShareBound()
- TestClashFreeSubst. testMultiSubst()
- TestClashFreeSubst. testShare()
- TestClashFreeSubst. testShareWary()
- TestClashFreeSubst. testSubst()
- TestClashFreeSubst. testSubstInSubstTerm()
- TestClashFreeSubst. testSubstWary()
- TestClashFreeSubst. testWary0()
- TestClashFreeSubst. testWary1()
- TestClashFreeSubst. testWary2()
- TestClashFreeSubst. xtestMultiClash()
- TestClashFreeSubst. xtestMultiClash1()
- TestLocalSymbols. testDoubleInstantiation()
- TestLocalSymbols. testSkolemization()
- TestPosInOcc. testIterator()
- TestPosInOcc. testReplaceConstrainedFormula()
- TestSemisequent. testContains()
- TestSemisequent. testContainsEquals()
- TestSemisequent. testEquals()
- TestSemisequent. testGet()
- TestSemisequent. testImmutable()
- TestSemisequent. testListInsert()
- TestSemisequent. testListInsertInMid()
- TestSemisequent. testListReplace()
- TestSemisequent. testListReplaceAddRedundantList()
- TestSemisequent. testNoDuplicates()
- TestSemisequent. testRemove()
- TestSemisequent. testRemoveOrder()
- TestSemisequent. testReplace()
- TestSemisequent. testUniqueEmpty()
- TestSemisequent. testindexOf()
- TestSyntacticalReplaceVisitor. test1()
- TestSyntacticalReplaceVisitor. testSubstitutionReplacement()
- TestTerm. testEqualsModRenaming()
- TestTerm. testEqualsModRenamingWithLabels()
- TestTerm. testFreeVars1()
- TestTerm. testFreeVars2()
- TestTerm. testFreeVars3()
- TestTerm. testFreeVars4()
- TestTerm. testIsContainsJavaBlockRecursive()
- TestTerm. testProgramElementEqualsModRenaming()
- TestTerm. testRigidness0()
- TestTermBuilder. testDoubleLongPatterns()
- TestTermBuilder. testFloatPatterns()
- TestTermBuilder. testNumberIsNegativeInt()
- TestTermBuilder. testNumberIsPositiveInt()
- TestTermBuilder. testNumberIsVeryBigPositiveInteger()
- TestTermBuilder. testNumberIsVerySmallNegativeInteger()
- TestTermFactory. testBoxTerm()
- TestTermFactory. testCaching()
- TestTermFactory. testConstantTrue()
- TestTermFactory. testDiamondTerm()
- TestTermFactory. testJunctorTerm()
- TestTermFactory. testJunctorTermWithWrongArity()
- TestTermFactory. testNegationTerm()
- TestTermFactory. testQuantifierTerm()
- TestTermFactory. testQuantifierWithNoBoundSubTerms()
- TestTermFactory. testSimplePredicate()
- TestTermFactory. testSubSorts1()
- TestTermFactory. testSubSortsEquals()
- TestTermFactory. testSubSortsSubst()
- TestTermFactory. testSubstitutionTerm()
- TestTermFactory. testSubtermsForLogicVariable()
- TestTermFactory. testWithInvalidSubformulae()
- TestTermFactory. testWrongArity()
- TestTermFactory. testWrongSorts()
- TestTermFactory. testWrongSubstTermForLogicVariable()
- TestTermLabelManager. testGetSupportedTermLabelNames()
- TestTermLabelManager. testInstantiateLabels_applicationTermPolicies()
- TestTermLabelManager. testInstantiateLabels_childAndGrandchildPolicies_allRules()
- TestTermLabelManager. testInstantiateLabels_childAndGrandchildPolicies_ruleSpecific()
- TestTermLabelManager. testInstantiateLabels_directChildPolicies_allRules()
- TestTermLabelManager. testInstantiateLabels_directChildPolicies_ruleSpecific()
- TestTermLabelManager. testInstantiateLabels_modalityTermPolicies()
- TestTermLabelManager. testInstantiateLabels_taclet()
- TestTermLabelManager. testInstantiateLabels_updates_allRules()
- TestTermLabelManager. testInstantiateLabels_updates_ruleSpecific()
- TestTermLabelManager. testParseLabel()
- TestTermLabelManager. testrefactorGoal_childrenAndGrandchildren_allRules()
- TestTermLabelManager. testrefactorGoal_childrenAndGrandchildren_ruleSpecific()
- TestTermLabelManager. testrefactorGoal_directChildren_allRules()
- TestTermLabelManager. testrefactorGoal_directChildren_ruleSpecific()
- TestTermLabelManager. testrefactorGoal_none_allRules()
- TestTermLabelManager. testrefactorGoal_none_ruleSpecific()
- TestTermLabelManager. testrefactorGoal_sequent_allRules()
- TestTermLabelManager. testrefactorGoal_sequent_ruleSpecific()
- FocusCommandTest. testSelectionWithLabels()
- FocusCommandTest. testSimpleSelection()
- TestProofScriptCommand. [1] unhide.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/unhide.props
- TestProofScriptCommand. [2] unhide2.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/unhide2.props
- TestProofScriptCommand. [3] rule.exc.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/rule.exc.props
- TestProofScriptCommand. [4] selectFormula.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/selectFormula.props
- TestProofScriptCommand. [5] hide.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/hide.props
- TestProofScriptCommand. [6] andRight.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/andRight.props
- TestProofScriptCommand. [7] hide.exc.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/hide.exc.props
- RewriteTest. testLessTransitive()
- RewriteTest. testTransitive()
- ExprTest. [10] -5
- ExprTest. [11] 1 + 1 = 2
- ExprTest. [12] \if (3=4) \then (1) \else (2)
- ExprTest. [13] \if (3=4 & 1=1) \then (\if (3=4) \then (1) \else (2)) \else (2)
- ExprTest. [14] aa + bb*cc
- ExprTest. [15] aa%bb*cc < -123
- ExprTest. [16] \forall int x; true
- ExprTest. [17] \forall numbers x; x = x
- ExprTest. [18] (int)3+2
- ExprTest. [19] 1.f + 1f = 20e-1f * (2f-1f)
- ExprTest. [1] (bprod{int y;}(1, 2, y) = 0)
- ExprTest. [20] 1.d + 1d <= 20e+1d * .01d
- ExprTest. [21] 1f <= 2f
- ExprTest. [22] 2d > 1d
- ExprTest. [23] seqEmpty + seqEmpty
- ExprTest. [2] 1 = 1 -> 2 = 2
- ExprTest. [3] \< { int x = 1; } \> x=1
- ExprTest. [4] \<{ int x = 1; {int s = 2;} }\> x=x
- ExprTest. [5] true
- ExprTest. [6] true & false
- ExprTest. [7] 0
- ExprTest. [8] 1
- ExprTest. [9] 42
- ParseLDTsTests. testLDT()
- ParseLDTsTests. testSR()
- TestTacletEquality. initializationError
- TestDeclParser. testArrayDecl()
- TestDeclParser. testFunctionDecl()
- TestDeclParser. testGenericSortDecl1()
- TestDeclParser. testGenericSortDecl2()
- TestDeclParser. testGenericSortDecl3()
- TestDeclParser. testGenericSortDecl4()
- TestDeclParser. testGenericSortDecl6()
- TestDeclParser. testHeurDecl()
- TestDeclParser. testPredicateDecl()
- TestDeclParser. testProxySortDecl()
- TestDeclParser. testSVDecl()
- TestDeclParser. testSortDecl()
- TestIntLiteralParsing. initializationError
- TestIntLiteralParsing. initializationError
- TestIntLiteralParsing. initializationError
- TestIntLiteralParsing. initializationError
- TestIntLiteralParsing. initializationError
- TestJMLParserAssociativity. testLeftAssociativity()
- TestParser. testConstantEvaluationError()
- TestParser. testGenericSort()
- TestParser. testIssue1566()
- TestTacletParser. testAllRight()
Ignored tests
Packages
| Package | Tests | Failures | Ignored | Duration | Success rate |
|---|---|---|---|---|---|
| default-package | 1 | 1 | 0 | 40m21.81s | 0% |
| de.uka.ilkd.key.java | 7 | 6 | 0 | 3.440s | 14% |
| de.uka.ilkd.key.java.visitor | 1 | 1 | 0 | 0.356s | 0% |
| de.uka.ilkd.key.logic | 138 | 90 | 0 | 3m24.96s | 34% |
| de.uka.ilkd.key.macros.scripts | 11 | 9 | 0 | 1.748s | 18% |
| de.uka.ilkd.key.macros.scripts.meta | 5 | 2 | 0 | 0.347s | 60% |
| de.uka.ilkd.key.nparser | 26 | 26 | 0 | 2.017s | 0% |
| de.uka.ilkd.key.parser | 27 | 22 | 4 | 36m37.77s | 4% |