Test Summary
|
56%
successful |
Failed tests
- TestExecutionVariableExtractor. testVariableArrayIndex()
- TestExecutionVariableExtractor. testVariablesArrayCreationInstanceTest()
- TestExecutionVariableExtractor. testVariablesArrayCreationTest()
- TestExecutionVariableExtractor. testVariablesConditionalValuesTest()
- TestExecutionVariableExtractor. testVariablesEmptyArrayCreationTest()
- TestExecutionVariableExtractor. testVariablesLocalVariablesTest()
- TestExecutionVariableExtractor. testVariablesNonSimpleArrayAssignmentTest()
- TestExecutionVariableExtractor. testVariablesWithQuantifier()
- TestParallelSiteProofs. testProofFile()
- TestSymbolicExecutionTreeBuilder. testAllNodeTypesTest_JavaProfile()
- TestSymbolicExecutionTreeBuilder. testAllNodeTypesTest_JavaProfile_NoOneStepSimplification()
- TestSymbolicExecutionTreeBuilder. testAllNodeTypesTest_SymbolicExecutionProfile()
- TestSymbolicExecutionTreeBuilder. testAssumesUserInputTest()
- TestSymbolicExecutionTreeBuilder. testBlockContractAssignableEverything()
- TestSymbolicExecutionTreeBuilder. testBlockContractAssignableLocationNotRequested()
- TestSymbolicExecutionTreeBuilder. testBlockContractAssignableRequestedLocation()
- TestSymbolicExecutionTreeBuilder. testBlockContractParamRemaned()
- TestSymbolicExecutionTreeBuilder. testBlockContractPreconditionNotVerified()
- TestSymbolicExecutionTreeBuilder. testBlockContractThisTest()
- TestSymbolicExecutionTreeBuilder. testBlockContractVarRenamedLater()
- TestSymbolicExecutionTreeBuilder. testBlockContractWithException()
- TestSymbolicExecutionTreeBuilder. testBlockContractWithExceptionPostconditionNotVerified()
- TestSymbolicExecutionTreeBuilder. testBlockContractWithReturn()
- TestSymbolicExecutionTreeBuilder. testBlockContractWithReturnPostconditionNotVerified()
- TestSymbolicExecutionTreeBuilder. testBranchStatementBlockTest_recursive()
- TestSymbolicExecutionTreeBuilder. testConstraintsAfterUsedLoopInvariant()
- TestSymbolicExecutionTreeBuilder. testConstraintsOfAppliedMethodContract()
- TestSymbolicExecutionTreeBuilder. testDoWhileFlaseTest()
- TestSymbolicExecutionTreeBuilder. testDoWhileTest()
- TestSymbolicExecutionTreeBuilder. testExceptionalMethodReturnTest()
- TestSymbolicExecutionTreeBuilder. testFunctionalDoWhileTest()
- TestSymbolicExecutionTreeBuilder. testFunctionalForTest()
- TestSymbolicExecutionTreeBuilder. testFunctionalWhileTest()
- TestSymbolicExecutionTreeBuilder. testIdenticalTermsDuringProof()
- TestSymbolicExecutionTreeBuilder. testJoinTestAfterAssignment()
- TestSymbolicExecutionTreeBuilder. testJoinTestAfterBranchCondition()
- TestSymbolicExecutionTreeBuilder. testJoinTestAfterBranchConditionWithWeakeningGoal()
- TestSymbolicExecutionTreeBuilder. testJoinTestAfterBranchConditionWithWeakeningGoalAndSubgoals()
- TestSymbolicExecutionTreeBuilder. testJoinTestAfterBranchConditionWithWeakeningGoalNotVerified()
- TestSymbolicExecutionTreeBuilder. testLoopInvariantMethodReturnInDifferentModalities()
- TestSymbolicExecutionTreeBuilder. testLoopIteration_LoopWithMethod()
- TestSymbolicExecutionTreeBuilder. testMethodCallOnObjectWithException()
- TestSymbolicExecutionTreeBuilder. testMethodCallReturnTests()
- TestSymbolicExecutionTreeBuilder. testMethodCallStack()
- TestSymbolicExecutionTreeBuilder. testNestedDoWhileTest()
- TestSymbolicExecutionTreeBuilder. testNestedLoopsWithContinue()
- TestSymbolicExecutionTreeBuilder. testPrettyPrinting_Disabled()
- TestSymbolicExecutionTreeBuilder. testPrettyPrinting_Enabled()
- TestSymbolicExecutionTreeBuilder. testSimpleIfNoConditionSimplification()
- TestSymbolicExecutionTreeBuilder. testSimpleMethodCallStack()
- TestSymbolicExecutionTreeBuilder. testStaticInstanceFieldChanged()
- TestSymbolicExecutionTreeBuilder. testUnicode_Disabled()
- TestSymbolicExecutionTreeBuilder. testUnicode_Enabled()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantArrayAverage()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantArraySizeDoWhile()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantLoopSplittingCondition()
- TestSymbolicExecutionTreeBuilder. testUseLoopInvariantWithoutDecreasing()
- TestSymbolicExecutionTreeBuilder. testUseOperationContractStatementsInImpliciteConstructor()
- TestSymbolicExecutionTreeBuilder. testVariablesArrayCreationInstanceTest()
- TestSymbolicExecutionTreeBuilder. testVariablesArrayCreationTest()
- TestSymbolicExecutionTreeBuilder. testVariablesArrayTest()
- TestSymbolicExecutionTreeBuilder. testVariablesEmptyArrayCreationTest()
- TestSymbolicExecutionTreeBuilder. testVariablesInstanceVariableTest()
- TestSymbolicExecutionTreeBuilder. testVariablesLocalTest()
- TestSymbolicExecutionTreeBuilder. testVariablesNonSimpleArrayAssignmentTest()
- TestSymbolicExecutionTreeBuilder. testVerifyMin()
- TestSymbolicExecutionTreeBuilder. testVerifyMinTrueBranch()
- TestSymbolicExecutionTreeBuilder. testVerifyNumberNormal()
- TestSymbolicExecutionTreeBuilder. testWhileWithMethodCallAsConditionOnObject()
- TestSymbolicExecutionTreeBuilder. testWhileWithMethodCallAsCondition_NoPreMethodContract()
- TestTruthValueEvaluationUtil. testAnd3_replaceKnown()
- TestTruthValueEvaluationUtil. testArraySumWhile()
- TestTruthValueEvaluationUtil. testArraySumWhile_NoOneStepSimplification()
- TestTruthValueEvaluationUtil. testDifferentBranchesTest()
- TestTruthValueEvaluationUtil. testEquivExample_NoOneStepSimplification()
- TestTruthValueEvaluationUtil. testExceptinalAssignableNothingTest()
- TestTruthValueEvaluationUtil. testExceptinalAssignableNothingTest_OSS()
- TestTruthValueEvaluationUtil. testJoinTestAfterBranchConditionWithWeakeningGoal()
- TestTruthValueEvaluationUtil. testMyInteger()
- TestTruthValueEvaluationUtil. testNotLastEvaluationGivesTruthValue()
- TestTruthValueEvaluationUtil. testSimpleInstanceMethodContractApplication()
- TestTruthValueEvaluationUtil. testSimpleInstanceMethodContractApplication_NoOneStepSimplification()
- TestTruthValueEvaluationUtil. testSimpleMethodContractApplication()
- TestTruthValueEvaluationUtil. testSimpleMethodContractApplication_NoOneStepSimplification()
- TestTruthValueEvaluationUtil. testTruthValueLabelBelowUpdatesDifferentToApplicationTerm()
- TestTruthValueEvaluationUtil. testUnderstandingProofs_Account()
- TestTruthValueEvaluationUtil. testUnderstandingProofs_ArrayUtil()
- TestTruthValueEvaluationUtil. testUnderstandingProofs_Calendar()
- TestTruthValueEvaluationUtil. testUnderstandingProofs_MyInteger()
- TestTruthValueEvaluationUtil. testValueRejectedFormula()
- TestFunctionalOperationContractPO. testDoubleValue()
- TestProgramMethodPO. testReturnMethod()
- TestProgramMethodPO. testReturnMethod_Precondition()
- TestProgramMethodPO. testVoidMethod()
- TestProgramMethodPO. testVoidMethod_Precondition()
- TestProgramMethodSubsetPO. testDoSomethingIf()
- TestProgramMethodSubsetPO. testDoSomethingIfWithSurroundingStatements()
- TestThinBackwardSlicer. testAliasChanged()
- TestThinBackwardSlicer. testAliasNotAvailable()
- TestThinBackwardSlicer. testAliasedByExecutionTest()
- TestThinBackwardSlicer. testAliasing()
- TestThinBackwardSlicer. testArrayIndexAsVariableFieldTest()
- TestThinBackwardSlicer. testArrayIndexSideeffectsAfter()
- TestThinBackwardSlicer. testArrayIndexSideeffectsBevore()
- TestThinBackwardSlicer. testArrayIndexVariableTest()
- TestThinBackwardSlicer. testBlockContractAssignableEverything()
- TestThinBackwardSlicer. testBlockContractAssignableLocationNotRequested()
- TestThinBackwardSlicer. testBlockContractAssignableRequestedLocation()
- TestThinBackwardSlicer. testEquivalenceClasses_Index_0()
- TestThinBackwardSlicer. testEquivalenceClasses_Index_0_no_OSS()
- TestThinBackwardSlicer. testEquivalenceClasses_Index_1()
- TestThinBackwardSlicer. testEquivalenceClasses_Index_1_no_OSS()
- TestThinBackwardSlicer. testFigure2Instance_right()
- TestThinBackwardSlicer. testFigure2Local_right()
- TestThinBackwardSlicer. testFigure2Param_right()
- TestThinBackwardSlicer. testFigure2_left()
- TestThinBackwardSlicer. testFigure2_right()
- TestThinBackwardSlicer. testInstanceFieldsAliased()
- TestThinBackwardSlicer. testLoopInvariantInListFieldsTest()
- TestThinBackwardSlicer. testLoopInvariantNestedListFieldsTest()
- TestThinBackwardSlicer. testLoopInvariantNotInListFieldsTest()
- TestThinBackwardSlicer. testLoopInvariantStarFieldsTest()
- TestThinBackwardSlicer. testMethodCallTest()
- TestThinBackwardSlicer. testMethodContractAssignableEverything()
- TestThinBackwardSlicer. testMethodContractAssignableLocationNotRequested()
- TestThinBackwardSlicer. testMethodContractAssignableRequestedLocation()
- TestThinBackwardSlicer. testNestedInstanceAccess_subResult()
- TestThinBackwardSlicer. testNestedInstanceFields()
- TestThinBackwardSlicer. testNotAliasedByExecutionTest()
- TestThinBackwardSlicer. testSimpleAliasChanged()
- TestThinBackwardSlicer. testSimpleArrayTest()
- TestThinBackwardSlicer. testSimpleInstanceFields()
- TestThinBackwardSlicer. testSimpleLoopInvariantTest()
- TestThinBackwardSlicer. testSimpleMultidimensionArrayTest()
- TestThinBackwardSlicer. testSimpleStaticLoopInvariantTest()
- TestThinBackwardSlicer. testValueChange()
- TestJavaWatchpointStopConditionWithHitCount. testBreakpointStopCondition()
- TestKeYWatchpointGlobalVariablesOnSatisfiable. testBreakpointStopCondition()
- TestKeYWatchpointGlobalVariablesOnTrueWithHitCount. testBreakpointStopCondition()
- TestKeYWatchpointMethodsOnSatisfiable. testBreakpointStopCondition()
- TestLineBreakpointStopConditionSimpleWithConditions. testBreakpointStopCondition()
- TestLineBreakpointStopConditionSimpleWithHitCount. testBreakpointStopCondition()
- TestLineBreakpointStopConditionSimpleWithLoopInvariant. testBreakpointStopCondition()
- TestMethodBreakpointWithConditions. testBreakpointStopCondition()
- TestMethodBreakpointWithHitCount. testBreakpointStopCondition()
- TestStepOverSymbolicExecutionTreeNodesStopCondition. testStepOverOnTwoBranches()
- TestSymbolicExecutionStrategy. testAliasTest_Array_AliasChecksImmediately()
- TestSymbolicExecutionStrategy. testBlockContractPreconditionNotVerified_SymbolicExecution()
- TestSymbolicExecutionStrategy. testBlockContractWithExceptionPostconditionNotVerified_SymbolicExecution()
- TestSymbolicExecutionStrategy. testBlockContractWithException_SymbolicExecution()
- TestSymbolicExecutionStrategy. testBlockContractWithReturnPostconditionNotVerified_SymbolicExecution()
- TestSymbolicExecutionStrategy. testBlockContractWithReturn_SymbolicExecution()
- TestSymbolicExecutionStrategy. testNonExecutionBranchHidingLoopInvariantWithSplittingQuery_hiding_off()
- TestSymbolicExecutionStrategy. testNonExecutionBranchHidingLoopInvariantWithSplittingQuery_hiding_side_proof()
- TestSymbolicExecutionStrategy. testNonExecutionBranchHidingQueryInPrecondition_hiding_side_proof()
- TestSymbolicExecutionStrategy. testNonExecutionBranchHidingQueryWithSideEffects_hiding_side_proof()
- TestSymbolicExecutionStrategy. testNonExecutionBranchHidingSimpleIntQuery_mainWithSymbolicUpdates_hiding_side_proof()
- TestSymbolicExecutionStrategy. testNonExecutionBranchHidingSimpleIntQuery_main_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 | 90 | 39 | 17m8.44s | 63% |
| de.uka.ilkd.key.symbolic_execution.testcase.po | 20 | 7 | 0 | 2m21.07s | 65% |
| de.uka.ilkd.key.symbolic_execution.testcase.slicing | 44 | 39 | 0 | 2m29.38s | 11% |
| de.uka.ilkd.key.symbolic_execution.testcase.strategy | 43 | 22 | 0 | 3m36.00s | 48% |
| de.uka.ilkd.key.symbolic_execution.testcase.util | 8 | 0 | 0 | 4.778s | 100% |