Test Summary
|
71%
successful |
Failed tests
- TestExecutionVariableExtractor. testVariableArrayIndex()
- TestExecutionVariableExtractor. testVariablesSimpleCycle()
- TestExecutionVariableExtractor. testVariablesWithQuantifier()
- TestSymbolicExecutionTreeBuilder. testAllNodeTypesTest_JavaProfile()
- TestSymbolicExecutionTreeBuilder. testAllNodeTypesTest_JavaProfile_NoOneStepSimplification()
- TestSymbolicExecutionTreeBuilder. testAllNodeTypesTest_SymbolicExecutionProfile()
- TestSymbolicExecutionTreeBuilder. testArraySumWhileWithBreak()
- TestSymbolicExecutionTreeBuilder. testArraySumWhileWithContinue()
- TestSymbolicExecutionTreeBuilder. testArraySumWhileWithException()
- TestSymbolicExecutionTreeBuilder. testArraySumWhileWithReturn()
- TestSymbolicExecutionTreeBuilder. testBlockContractAssignableEverything()
- TestSymbolicExecutionTreeBuilder. testBlockContractAssignableLocationNotRequested()
- TestSymbolicExecutionTreeBuilder. testBlockContractAssignableRequestedLocation()
- TestSymbolicExecutionTreeBuilder. testBlockContractParamRemaned()
- TestSymbolicExecutionTreeBuilder. testBlockContractVarRenamedLater()
- TestSymbolicExecutionTreeBuilder. testBlockContractWithException()
- TestSymbolicExecutionTreeBuilder. testBlockContractWithExceptionPostconditionNotVerified()
- TestSymbolicExecutionTreeBuilder. testBlockContractWithReturn()
- TestSymbolicExecutionTreeBuilder. testBlockContractWithReturnPostconditionNotVerified()
- TestSymbolicExecutionTreeBuilder. testConstraintsAfterUsedLoopInvariant()
- TestSymbolicExecutionTreeBuilder. testConstraintsOfAppliedMethodContract()
- TestSymbolicExecutionTreeBuilder. testDoWhileFlaseTest()
- TestSymbolicExecutionTreeBuilder. testDoWhileTest()
- TestSymbolicExecutionTreeBuilder. testExceptionalMethodReturnTestWithLoop()
- TestSymbolicExecutionTreeBuilder. testForEachTest()
- TestSymbolicExecutionTreeBuilder. testForFalseTest()
- TestSymbolicExecutionTreeBuilder. testForTest()
- TestSymbolicExecutionTreeBuilder. testFunctionalDoWhileTest()
- TestSymbolicExecutionTreeBuilder. testFunctionalForTest()
- TestSymbolicExecutionTreeBuilder. testFunctionalWhileTest()
- TestSymbolicExecutionTreeBuilder. testIdenticalTermsDuringProof()
- TestSymbolicExecutionTreeBuilder. testInstanceContractTest_mainResult()
- TestSymbolicExecutionTreeBuilder. testInstanceContractTest_mainResultNotSpecified()
- TestSymbolicExecutionTreeBuilder. testLoopInvariantAndOperationContractStrictlyPure()
- TestSymbolicExecutionTreeBuilder. testLoopInvariantMethodReturnInDifferentModalities()
- TestSymbolicExecutionTreeBuilder. testLoopIteration_LoopStatementCopied()
- TestSymbolicExecutionTreeBuilder. testLoopIteration_LoopStatementReused()
- TestSymbolicExecutionTreeBuilder. testLoopIteration_LoopWithMethod()
- TestSymbolicExecutionTreeBuilder. testLoopStatementBlockTest_nestedLoop()
- TestSymbolicExecutionTreeBuilder. testLoopStatementBlockTest_simpleLoop()
- TestSymbolicExecutionTreeBuilder. testNestedDoWhileTest()
- TestSymbolicExecutionTreeBuilder. testNestedForTest()
- TestSymbolicExecutionTreeBuilder. testNestedLoopsWithContinue()
- TestSymbolicExecutionTreeBuilder. testNestedWhileTest()
- TestSymbolicExecutionTreeBuilder. testPrettyPrinting_Disabled()
- TestSymbolicExecutionTreeBuilder. testPrettyPrinting_Enabled()
- TestSymbolicExecutionTreeBuilder. testStaticContractTest_mainResult()
- TestSymbolicExecutionTreeBuilder. testStaticContractTest_mainResultNotSpecified()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantArrayAverage()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantArraySizeDoWhile()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantArraySizeWhile()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantArraySumFor()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantArraySumForEach()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantArraySumWhile()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantArraySumWhileInitiallyInvalid()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantTwoLoops()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantWithoutDecreasing()
- TestSymbolicExecutionTreeBuilder. testUseOperationContractQueryTest()
- TestSymbolicExecutionTreeBuilder. testUseOperationContractStatementsInImpliciteConstructor()
- TestSymbolicExecutionTreeBuilder. testUseOperationContractVariableNestedOperationContractUse()
- TestSymbolicExecutionTreeBuilder. testVerifiedTest_loop()
- TestSymbolicExecutionTreeBuilder. testVerifiedTest_notLoop()
- TestSymbolicExecutionTreeBuilder. testVoidWhileWithReturn()
- TestSymbolicExecutionTreeBuilder. testWhileFalseTest()
- TestSymbolicExecutionTreeBuilder. testWhileTest()
- TestSymbolicExecutionTreeBuilder. testWhileWithLoopInvariantInCondition()
- TestSymbolicExecutionTreeBuilder. testWhileWithMethodCallAsConditionOnObject()
- TestSymbolicExecutionTreeBuilder. testWhileWithMethodCallAsCondition_NoPreExpandMethods()
- TestSymbolicExecutionTreeBuilder. testWhileWithMethodCallAsCondition_NoPreMethodContract()
- TestSymbolicExecutionTreeBuilder. testWhileWithMethodCallAsCondition_preExpandMethods()
- TestSymbolicExecutionTreeBuilder. testWhileWithMethodCallAsCondition_preMethodContract()
- TestTruthValueEvaluationUtil. testArraySumWhile()
- TestTruthValueEvaluationUtil. testArraySumWhile_NoOneStepSimplification()
- TestTruthValueEvaluationUtil. testMyInteger()
- TestTruthValueEvaluationUtil. testSimpleInstanceMethodContractApplication()
- TestTruthValueEvaluationUtil. testSimpleInstanceMethodContractApplication_NoOneStepSimplification()
- TestTruthValueEvaluationUtil. testSimpleMethodContractApplication()
- TestTruthValueEvaluationUtil. testSimpleMethodContractApplication_NoOneStepSimplification()
- TestTruthValueEvaluationUtil. testUnderstandingProofs_Account()
- TestTruthValueEvaluationUtil. testUnderstandingProofs_ArrayUtil()
- TestTruthValueEvaluationUtil. testUnderstandingProofs_Calendar()
- TestTruthValueEvaluationUtil. testUnderstandingProofs_MyInteger()
- TestThinBackwardSlicer. testArrayIndexAsVariableFieldTest()
- TestThinBackwardSlicer. testArrayIndexSideeffectsAfter()
- TestThinBackwardSlicer. testArrayIndexSideeffectsBevore()
- TestThinBackwardSlicer. testArrayIndexVariableTest()
- TestThinBackwardSlicer. testBlockContractAssignableEverything()
- TestThinBackwardSlicer. testBlockContractAssignableLocationNotRequested()
- TestThinBackwardSlicer. testBlockContractAssignableRequestedLocation()
- TestJavaWatchpointStopConditionWithHitCount. testBreakpointStopCondition()
- TestKeYWatchpointGlobalVariablesOnSatisfiable. testBreakpointStopCondition()
- TestKeYWatchpointGlobalVariablesOnTrueWithHitCount. testBreakpointStopCondition()
- TestKeYWatchpointMethodsOnSatisfiable. testBreakpointStopCondition()
- TestLineBreakpointStopConditionSimpleWithConditions. testBreakpointStopCondition()
- TestLineBreakpointStopConditionSimpleWithHitCount. testBreakpointStopCondition()
- TestLineBreakpointStopConditionSimpleWithLoopInvariant. testBreakpointStopCondition()
- TestMethodBreakpointWithConditions. testBreakpointStopCondition()
- TestMethodBreakpointWithHitCount. testBreakpointStopCondition()
- TestSymbolicExecutionStrategy. testNonExecutionBranchHidingArraysIndexOf_hiding_off()
- TestSymbolicExecutionStrategy. testNonExecutionBranchHidingArraysIndexOf_hiding_side_proof()
- TestSymbolicExecutionStrategy. testNonExecutionBranchHidingLoopInvariantWithSplittingQuery_hiding_off()
- TestSymbolicExecutionStrategy. testNonExecutionBranchHidingLoopInvariantWithSplittingQuery_hiding_side_proof()
Ignored tests
- TestParallelSiteProofs. xxxtestNewProof()
- TestSymbolicExecutionTreeBuilder. testComplexConstructorTest()
- TestSymbolicLayoutExtractor. testArrayCreationTest()
- TestSymbolicLayoutExtractor. testArrayIndexReadAccess()
- TestSymbolicLayoutExtractor. testArrayIndexWriteAccess()
- TestSymbolicLayoutExtractor. testArrayInstanceCreationTest()
- TestSymbolicLayoutExtractor. testAssociationSourceIsNotRepresentativeTermOfEquivalenceClass()
- TestSymbolicLayoutExtractor. testEmptyArrayCreationTest()
- TestSymbolicLayoutExtractor. testEmptyPathConditionAndNoUpdates()
- TestSymbolicLayoutExtractor. testExistsQuantifierTest()
- TestSymbolicLayoutExtractor. testInstanceCreationTest()
- TestSymbolicLayoutExtractor. testInstanceCreationTest_OnReturnNode()
- TestSymbolicLayoutExtractor. testIntegerConditionTest()
- TestSymbolicLayoutExtractor. testIsInstanceTest()
- TestSymbolicLayoutExtractor. testIsNullTest()
- TestSymbolicLayoutExtractor. testMultiArrayIndexReadWriteAccess()
- TestSymbolicLayoutExtractor. testMyInteger()
- TestSymbolicLayoutExtractor. testObjectArrayIndexReadAccess()
- TestSymbolicLayoutExtractor. testObjectArrayIndexWriteAccess()
- TestSymbolicLayoutExtractor. testObjectConditionTest()
- TestSymbolicLayoutExtractor. testOneAssignmentTest()
- TestSymbolicLayoutExtractor. testSimpleArrayCreation()
- TestSymbolicLayoutExtractor. testSimpleArrayLength()
- TestSymbolicLayoutExtractor. testSimpleLinkedArrays()
- TestSymbolicLayoutExtractor. testSimpleLinkedOjbects()
- TestSymbolicLayoutExtractor. testSimpleLinkedOjbectsDeletion()
- TestSymbolicLayoutExtractor. testSimpleLinkedOjbectsDeletionPreCondition()
- TestSymbolicLayoutExtractor. testSimpleLinkedOjbectsInsertion()
- TestSymbolicLayoutExtractor. testSimpleLinkedOjbectsInstanceVariable()
- TestSymbolicLayoutExtractor. testSimpleLinkedOjbectsPreCondition()
- TestSymbolicLayoutExtractor. testSimpleStaticAttributes()
- TestSymbolicLayoutExtractor. testStaticMember_OnReturnNode()
- TestSymbolicLayoutExtractor. testVariableArrayIndex()
- TestSymbolicLayoutExtractor. testWithOperationContracts()
- TestTruthValueEvaluationUtil. IGNORE_testAddingOfLabeledSubtree()
- TestTruthValueEvaluationUtil. IGNORE_testArrayUtil()
- TestTruthValueEvaluationUtil. IGNORE_testArrayUtil_NoOneStepSimplification()
- TestTruthValueEvaluationUtil. IGNORE_testAssignableAndLoop()
- TestTruthValueEvaluationUtil. IGNORE_testBlockContractMagic42()
Packages
| Package | Tests | Failures | Ignored | Duration | Success rate |
|---|---|---|---|---|---|
| de.uka.ilkd.key.symbolic_execution.testcase | 285 | 82 | 39 | 16m32.46s | 66% |
| de.uka.ilkd.key.symbolic_execution.testcase.po | 20 | 0 | 0 | 1m57.30s | 100% |
| de.uka.ilkd.key.symbolic_execution.testcase.slicing | 44 | 7 | 0 | 2m3.60s | 84% |
| de.uka.ilkd.key.symbolic_execution.testcase.strategy | 43 | 13 | 0 | 2m48.86s | 69% |
| de.uka.ilkd.key.symbolic_execution.testcase.util | 8 | 0 | 0 | 4.155s | 100% |