Test Summary
|
42%
successful |
Failed tests
- ProofJavaProgramFactoryTest. testAttachCommentsCompilationUnit_AssertsFalse()
- ProofJavaProgramFactoryTest. testAttachCommentsCompilationUnit_LockSpec()
- ProofJavaProgramFactoryTest. testAttachCommentsCompilationUnit_SetStatements()
- ProofJavaProgramFactoryTest. testAttachCommentsCompilationUnit_SmansEtAlArrayList()
- ProofJavaProgramFactoryTest. testAttachCommentsCompilationUnit_Steinhofel1()
- TestContextStatementBlock. testContextTermInstantiation()
- TestJavaCardDLJavaExtensions. testMethodFrameRedirectsScope()
- TestJavaInfo. initializationError
- TestRecoder2KeY. testJBlocks()
- TestRecoder2KeY. testJClasses()
- TestRecoder2KeY. testReadBlockWithContext()
- 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()
- TestPosInProgram. getProgram()
- 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()
- TestVariableNamer. testInnerRename()
- TestVariableNamer. testInnerRenameUniqueness()
- TestVariableNamer. testNameProposals()
- FocusCommandTest. testSelectionWithLabels()
- FocusCommandTest. testSimpleSelection()
- TestProofScriptCommand. [1] andRight.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\andRight.props
- TestProofScriptCommand. [2] hide.exc.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\hide.exc.props
- TestProofScriptCommand. [3] hide.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\hide.props
- TestProofScriptCommand. [4] rule.exc.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\rule.exc.props
- TestProofScriptCommand. [5] selectFormula.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\selectFormula.props
- TestProofScriptCommand. [6] unhide.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\unhide.props
- TestProofScriptCommand. [7] unhide2.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\unhide2.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()
- TestParallelParsing. testLoadingOfTwoDifferentProofFiles()
- TestParser. testConstantEvaluationError()
- TestParser. testGenericSort()
- TestParser. testIssue1566()
- TestTacletParser. testAllLeft()
- TestTacletParser. testAllRight()
- TestTacletParser. testClose()
- TestTacletParser. testContraposition()
- TestTacletParser. testCut()
- TestTacletParser. testExConjSplit()
- TestTacletParser. testFIdempotent()
- TestTacletParser. testFreeReplacewithVariables()
- TestTacletParser. testImpLeft()
- TestTacletParser. testImpRight()
- TestTacletParser. testMakeInsertEq()
- TestTacletParser. testSchemaJava0()
- TestTacletParser. testSchemaJava1()
- TestTacletParser. testSchemaJava10()
- TestTacletParser. testSchemaJava11()
- TestTacletParser. testSchemaJava2()
- TestTacletParser. testSchemaJava4()
- TestTacletParser. testSchemaJava6()
- TestTacletParser. testSchemaJava8()
- TestTacletParser. testVarcondNew()
- TestTermParser. test1()
- TestTermParser. test10()
- TestTermParser. test11()
- TestTermParser. test12()
- TestTermParser. test13()
- TestTermParser. test14()
- TestTermParser. test1a()
- TestTermParser. test2()
- TestTermParser. test3()
- TestTermParser. test5()
- TestTermParser. test6()
- TestTermParser. test7()
- TestTermParser. test8()
- TestTermParser. test9()
- TestTermParser. testAmbigiousFuncVarPred()
- TestTermParser. testAttributeOnObject()
- TestTermParser. testAttributeWithSpecifiedSortOnObject()
- TestTermParser. testBindingUpdateTerm()
- TestTermParser. testBindingUpdateTerm_1()
- TestTermParser. testBindingUpdateTerm_3()
- TestTermParser. testBindingUpdateTerm_4()
- TestTermParser. testBindingUpdateTerm_5()
- TestTermParser. testBindingUpdateTerm_6()
- TestTermParser. testBindingUpdateTerm_7()
- TestTermParser. testBindingUpdateTerm_8()
- TestTermParser. testCast()
- TestTermParser. testIfThenElse()
- TestTermParser. testInfix1()
- TestTermParser. testInfix2()
- TestTermParser. testInfix3()
- TestTermParser. testInfix4()
- TestTermParser. testJavaAttributeAccessBoth_1()
- TestTermParser. testJavaAttributeAccessBoth_2()
- TestTermParser. testJavaAttributeAccessBoth_3()
- TestTermParser. testJavaAttributeAccess_4()
- TestTermParser. testJavaQueryAndAttribute_all()
- TestTermParser. testJavaStaticQuery()
- TestTermParser. testJavaStaticQueryWithParameter()
- TestTermParser. testNegativeLiteralParsing1()
- TestTermParser. testNegativeLiteralParsing2()
- TestTermParser. testNegativeLiteralParsing3()
- TestTermParser. testNotEqual()
- TestTermParser. testParsingArray()
- TestTermParser. testParsingArrayCombination()
- TestTermParser. testProgramVariables()
- TestTermParser. xtestBindingUpdateTermOldBindingAlternative()
- TestTermParser. xtestParsingArrayWithSpaces()
- TestTermParserHeap. testAccessStaticMembers()
- TestTermParserHeap. testAllFieldsSelector()
- TestTermParserHeap. testAtOperator_1()
- TestTermParserHeap. testAtOperator_2()
- TestTermParserHeap. testAtOperator_3()
- TestTermParserHeap. testAtOperator_4()
- TestTermParserHeap. testAtOperator_5()
- TestTermParserHeap. testAtOperator_6()
- TestTermParserHeap. testAtOperator_7()
- TestTermParserHeap. testAtOperator_8()
- TestTermParserHeap. testBracketHeapUpdate()
- TestTermParserHeap. testBugResettingCounter()
- TestTermParserHeap. testGenericObjectProperties()
- TestTermParserHeap. testLocationSets()
- TestTermParserHeap. testParsePrettyPrintedSelect()
- TestTermParserHeap. testQuantifiedSelect()
- TestTermParserHeap. testQueryBasic_1()
- TestTermParserHeap. testQueryBasic_10()
- TestTermParserHeap. testQueryBasic_11()
- TestTermParserHeap. testQueryBasic_2()
- TestTermParserHeap. testQueryBasic_3()
- TestTermParserHeap. testQueryBasic_4()
- TestTermParserHeap. testQueryBasic_5()
- TestTermParserHeap. testQueryBasic_6()
- TestTermParserHeap. testQueryBasic_7()
- TestTermParserHeap. testQueryBasic_8()
- TestTermParserHeap. testQueryBasic_9()
- TestTermParserHeap. testQueryInheritance_1()
- TestTermParserHeap. testQueryInheritance_2()
- TestTermParserHeap. testQueryInheritance_3()
- TestTermParserHeap. testQueryInheritance_4()
- TestTermParserHeap. testQueryInheritance_5()
- TestTermParserHeap. testQueryInheritance_6()
- TestTermParserHeap. testQueryInheritance_7()
- TestTermParserHeap. testQueryInheritance_8()
- TestTermParserHeap. testQueryInheritance_9()
- TestTermParserHeap. testStore()
- TestTermParserHeap. testUnknownConstant()
- TestTermParserHeap. testVerifyExceptionIfAtOperatorNotPreceededBySelectTerm()
- TestTermParserSorts. testParseIntegerArgs()
- TestTermParserSorts. testParseSequencePrettySyntax()
- PrettyPrinterTest. printLocationVariable()
- TestGoal. testSetBack0()
- TestGoal. testSetBack1()
- TestOneStepSimplifier. loadWithRestriction()
- TestProofTree. testLeaves()
- TestTacletIndex. testMatchConflictOccurs()
- TestTacletIndex. testNoMatchingFindRule()
- TestTacletIndex. testNotFreeInYConflict()
- TestTacletIndex. testShownIfHeuristicFits()
- TestTermTacletAppIndex. testIndex0()
- TestTermTacletAppIndex. testIndex0WithCache()
- TestZipProofSaving. testZip()
- TestProofBundleIO. testComplexBundleGeneration()
- TestProofBundleIO. testSimpleBundleGeneration()
- TestApplyTaclet. testAddExistingFormulaAntec()
- TestApplyTaclet. testAddExistingFormulaSucc()
- TestApplyTaclet. testAddExistingFormulaTwoInAntec()
- TestApplyTaclet. testAddExistingFormulaTwoInAntec2()
- TestApplyTaclet. testAddExistingFormulaTwoInSucc()
- TestApplyTaclet. testAddExistingFormulaTwoInSucc2()
- TestApplyTaclet. testAddingRule()
- TestApplyTaclet. testAntecTacletWithoutIf()
- TestApplyTaclet. testBugBrokenApply()
- TestApplyTaclet. testBugEmptyBlock()
- TestApplyTaclet. testBugID176()
- TestApplyTaclet. testBugID177()
- TestApplyTaclet. testBugID188()
- TestApplyTaclet. testCatchList()
- TestApplyTaclet. testCompleteContextAddBug()
- TestApplyTaclet. testContextAdding()
- TestApplyTaclet. testIncompleteNoFindTacletApp()
- TestApplyTaclet. testIncompleteSuccTacletApp()
- TestApplyTaclet. testModalityLevel0()
- TestApplyTaclet. testModalityLevel1()
- TestApplyTaclet. testModalityLevel2()
- TestApplyTaclet. testNoFindTacletWithoutIf()
- TestApplyTaclet. testPrgTacletApp()
- TestApplyTaclet. testRemoveEmptyBlock()
- TestApplyTaclet. testRewriteTacletWithoutIf()
- TestApplyTaclet. testSuccTacletAllRight()
- TestApplyTaclet. testSuccTacletWithoutIf()
- TestApplyTaclet. testTacletVariableCollector()
- TestApplyTaclet. testTacletWithIf()
- TestCollisionResolving. testCollisionResolvingOfSchemaVariable()
- TestCollisionResolving. testCollisionResolvingWithContext()
- TestCollisionResolving. testNameConflict1()
- TestCollisionResolving. testNameConflictAfterInput()
- TestCollisionResolving. testNameConflictWithContextAfterInput()
- TestCollisionResolving. testVarNamespaceCreationWithContext()
- TestCollisionResolving. testVarNamespaceCreationWithPrefix()
- TestMatchTaclet. testBugsThathaveBeenRemoved()
- TestMatchTaclet. testCloseWithBoundRenaming()
- TestMatchTaclet. testConflict()
- TestMatchTaclet. testInsequentStateRestriction()
- TestMatchTaclet. testNoContextMatching()
- TestMatchTaclet. testPrefixMatching()
- TestMatchTaclet. testProgramMatch4()
- TestMatchTaclet. testProgramMatchEmptyBlock()
- TestMatchTaclet. testRWVarOccursFindAndIf()
- TestMatchTaclet. testRWVarOccursInAddAndIf()
- TestMatchTaclet. testUpdateMatch()
- TestMatchTaclet. testVarOccursInFindAndAddRule()
- TestMatchTaclet. testVarOccursInIfAndAddRule()
- TestMatchTaclet. testWithSubSortsTermSV()
- TestMatchTaclet. testWithSubSortsVariableSV()
- TestMatchTaclet. testXNotFreeInYConflict()
- TestSchemaModalOperators. testSchemaModalities1()
- TestSchemaModalOperators. testSchemaModalities2()
- TestSchemaModalOperators. testSchemaModalities3()
- TestSchemaModalOperators. testSchemaModalities4()
- TestDropEffectlessElementary. testDoubleAssignment()
- TestDropEffectlessElementary. testFaultyCase()
- TestDropEffectlessElementary. testSelfAssignments()
- TestGenericSortInstantiations. testGeneric1()
- TestGenericSortInstantiations. testGeneric2()
- TestGenericSortInstantiations. testGeneric2Array()
- TestGenericSortInstantiations. testGeneric3()
- TestGenericSortInstantiations. testGeneric4()
- TestGenericSortInstantiations. testGeneric5()
- TestGenericSortInstantiations. testGeneric6()
- TestGenericSortInstantiations. testNullsort()
- LoopScopeInvRuleTests. testDoAutomaticProofOfBenchmarkWithLabeledBreaksAndContinues()
- TestLegacyTacletMatch. testProgramMatch0()
- TestLegacyTacletMatch. testProgramMatch1()
- TestLegacyTacletMatch. testProgramMatch2()
- TestLegacyTacletMatch. testStatementListMatch()
- VMTacletMatcherTest. initializationError
- MergeRuleTests. testDoAutomaticGcdProofWithMergePointStatementAndBlockContract()
- MergeRuleTests. testDoAutomaticGcdProofWithMergePointStatements()
- MergeRuleTests. testDoManualGcdProof()
- MergeRuleTests. testLoadClosedGcdProofWithMergePointStatements()
- MergeRuleTests. testLoadGcdProof()
- MergeRuleTests. testLoadGcdProofWithPredAbstr()
- MergeRuleTests. testLoadGcdProofWithPredAbstrAndUserChoices()
- MergeRuleTests. testLoadProofWithDiffVarsWithSameNameAndMPS()
- MergeRuleTests. testMergeIndistinguishablePathConditionsWithFullAnonymization()
- MergeRuleTests. testMergeIndistinguishablePathConditionsWithITE()
- MergeRuleTests. testMergeThreeIndistinguishablePathConditionsWithITE()
- PredicateAbstractionLatticeTests. testCreateSignLatticeWithPredicates()
- PredicateAbstractionLatticeTests. testToAndFromString()
- TestProgramMetaConstructs. testBugId183()
- TestProgramMetaConstructs. testDoBreak()
- TestProgramMetaConstructs. testForInitUnfoldTransformer1()
- TestProgramMetaConstructs. testForInitUnfoldTransformer2()
- TestProgramMetaConstructs. testForInitUnfoldTransformer3()
- TestProgramMetaConstructs. testTypeOf()
- TestTacletBuild. test0()
- TestTacletBuild. testSchemavariablesInAddrulesRespectPrefix()
- TestTacletBuild. testUniquenessOfIfAndFindVarSVBothInIf()
- TestTacletBuild. testUniquenessOfIfAndFindVarSVsInFind()
- TestTacletBuild. testUniquenessOfIfAndFindVarSVsInIfAndFind()
- MasterHandlerTest. initializationError
- MasterHandlerTest. initializationError
- ProveSMTLemmasTest. [10] wellFormed.dl, \forall Heap h; \forall Object o; \forall Field f; (wellFormed(h) -> boolean::select(h, (java.lang.Object::select(h, o, f))<<Trigger>>, java.lang.Object::<created>) = TRUE | (java.lang.Object::select(h, o, f)) = null)
- ProveSMTLemmasTest. [11] jdiv.dl, \forall int divNum; \forall int divDenom; jdiv(divNum,divDenom) = \if (divNum >= 0) \then (div(divNum,divDenom)) \else (div(divNum*(-1),divDenom)*(-1))
- ProveSMTLemmasTest. [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false )
- ProveSMTLemmasTest. [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true )
- ProveSMTLemmasTest. [14] arrayRange.dl, \forall Object o; \forall Object o2; \forall Field f; \forall int lo; \forall int hi; (elementOf(o,f, arrayRange(o2, lo, hi))<<Trigger>> <-> o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi))
- ProveSMTLemmasTest. [15] seqConcat.dl, \forall int i; \forall Seq s1; \forall Seq s2; ( 0 <= i & i < seqLen(s1) + seqLen(s2) -> any::seqGet(seqConcat(s1, s2), i) = \if (i < seqLen(s1)) \then (any::seqGet(s1, i)) \else (any::seqGet(s2, i-seqLen(s1))))
- ProveSMTLemmasTest. [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0
- ProveSMTLemmasTest. [17] length.dl, \forall Object o; length(o) >= 0
- ProveSMTLemmasTest. [18] freshLocs.dl, \forall Heap h; \forall Object o; \forall Field f; ( elementOf(o,f,freshLocs(h))<<Trigger>> <-> o != null & !boolean::select(h,o,java.lang.Object::<created>)=TRUE )
- ProveSMTLemmasTest. [19] anon.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Heap h2; \forall LocSet ls; any::select(anon(h, ls, h2), o, f)<<Trigger>> = \if(elementOf(o, f, ls) & f != java.lang.Object::<created> | elementOf(o, f, freshLocs(h))) \then(any::select(h2, o, f)) \else(any::select(h, o, f))
- ProveSMTLemmasTest. [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom
- ProveSMTLemmasTest. [20] memset.dl, \forall Heap h; \forall LocSet s; \forall any x; \forall Object o; \forall Field f; any::select(memset(h, s, x), o, f)<<Trigger>> = \if(elementOf(o, f, s) & f != java.lang.Object::<created>) \then(x) \else(any::select(h, o, f))
- ProveSMTLemmasTest. [21] store.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; \forall any v; any::select(store(h,o,f,v), o2, f2)<<Trigger>> = \if(o = o2 & f = f2 & f != java.lang.Object::<created>) \then(v) \else(any::select(h, o2, f2))
- ProveSMTLemmasTest. [22] seqSub.dl.2, \forall Seq seq; \forall int from; \forall int to; seqLen(seqSub(seq, from, to)<<Trigger>>) = \if(from < to)\then(to - from)\else(0)
- ProveSMTLemmasTest. [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x
- ProveSMTLemmasTest. [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1
- ProveSMTLemmasTest. [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null)
- ProveSMTLemmasTest. [2] seqSub.dl, \forall Seq seq; \forall int from; \forall int to; \forall int idx; any::seqGet(seqSub(seq, from, to)<<Trigger>>, idx) = \if(0 <= idx & idx < (to - from)) \then(any::seqGet(seq, idx + from)) \else(seqGetOutside)
- ProveSMTLemmasTest. [3] seqGetOutside.dl, \forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside )
- ProveSMTLemmasTest. [4] singleton.dl, \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; ( elementOf(o,f, singleton(o2,f2))<<Trigger>> <-> o = o2 & f = f2 )
- ProveSMTLemmasTest. [5] create.dl, \forall Heap h; \forall Object o; \forall Object o2; \forall Field f; any::select(create(h, o), o2, f)<<Trigger>> = \if(o = o2 & o != null & f = java.lang.Object::<created>) \then(TRUE) \else(any::select(h, o2, f))
- ProveSMTLemmasTest. [6] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 )
- ProveSMTLemmasTest. [7] seqEmpty.dl, seqLen(seqEmpty) = 0
- ProveSMTLemmasTest. [8] union.dl, \forall Object o; \forall Field f; \forall LocSet l1; \forall LocSet l2; ( elementOf(o, f, union(l1, l2))<<Trigger>> <-> elementOf(o,f,l1) | elementOf(o,f,l2) )
- ProveSMTLemmasTest. [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2)
- ContractFactoryTest. testCombineDifferentAssignable()
- ContractFactoryTest. testCombineEmptyAssignable()
- ContractFactoryTest. testCombineEqualAssignable()
- TestJMLTranslator. testBsumBigInt()
- TestJMLTranslator. testBsumInt()
- TestJMLTranslator. testComplexExists()
- TestJMLTranslator. testComplexQueryResolving1()
- TestJMLTranslator. testComplexQueryResolving2()
- TestJMLTranslator. testComplexQueryResolving3()
- TestJMLTranslator. testCorrectImplicitThisResolution()
- TestJMLTranslator. testForAll()
- TestJMLTranslator. testForEx()
- TestJMLTranslator. testHexLiteral()
- TestJMLTranslator. testInfiniteUnion()
- TestJMLTranslator. testInfiniteUnion2()
- TestJMLTranslator. testIsInitialized()
- TestJMLTranslator. testLogicalExpression()
- TestJMLTranslator. testNonNullElements()
- TestJMLTranslator. testOld()
- TestJMLTranslator. testParenExpression()
- TestJMLTranslator. testPrimitiveField()
- TestJMLTranslator. testResultVar()
- TestJMLTranslator. testSelfVar()
- TestJMLTranslator. testSimpleQuery()
- TestJMLTranslator. testStaticQueryResolving()
- TestJMLTranslator. testSubtypeExpression()
- TestJMLTranslator. testSumParsing()
- TestJMLTranslator. testTrueTerm()
- 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()
- TestTriggersSet. testTrigger1()
- TestTacletTranslator. testNegativePolarity()
- TestTacletTranslator. testNoPolarity()
- TestTacletTranslator. testPositivePolarity()
- TestTacletTranslator. testPropositional1()
- TestTacletTranslator. testPropositional2()
- TestGenericRemovingLemmaGenerator. testRemovingGenericSorts()
- TestProofStarter. testDirectProof()
- TestProofStarter. testDirectProofWithOneStepSimplification()
Ignored tests
- TestRecoder2KeY. xtestFileInput()
- TestDeclParser. testAmbiguousDecls()
- TestDeclParser. testGenericSortDecl5()
- TestParser. testRelativeInclude()
- ParserMessageTest. verifyColumnNumber()
- ParserMessageTest. verifyLineNumber()
- ParserMessageTest. verifyMessage()
- TestTacletIndex. disabled_testNonInteractiveIsShownOnlyIfHeuristicIsMissed()
- TestProgramMetaConstructs. testASTWalker()
- TestCvc4. testAdd1()
- TestCvc4. testAllex1()
- TestCvc4. testAllex2()
- TestCvc4. testAllex3()
- TestCvc4. testAndnot()
- TestCvc4. testAndornot()
- TestCvc4. testAndornot2()
- TestCvc4. testBProd1()
- TestCvc4. testBProd2()
- TestCvc4. testBProd3()
- TestCvc4. testBSum1()
- TestCvc4. testBSum2()
- TestCvc4. testBSum3()
- TestCvc4. testBinderPred2()
- TestCvc4. testBinderPred3()
- TestCvc4. testEqual1()
- TestCvc4. testEqual2()
- TestCvc4. testEqui1()
- TestCvc4. testEqui2()
- TestCvc4. testImply()
- TestCvc4. testImply2()
- TestCvc4. testImply3()
- TestCvc4. testLogicalIte1()
- TestCvc4. testLogicalIte2()
- TestCvc4. testOrnot()
- TestCvc4. testSubsort1()
- TestCvc4. testSubsort2()
- TestZ3. testAdd1()
- TestZ3. testAllex1()
- TestZ3. testAllex2()
- TestZ3. testAllex3()
- TestZ3. testAndnot()
- TestZ3. testAndornot()
- TestZ3. testAndornot2()
- TestZ3. testBProd1()
- TestZ3. testBProd2()
- TestZ3. testBProd3()
- TestZ3. testBSum1()
- TestZ3. testBSum2()
- TestZ3. testBSum3()
- TestZ3. testBinderPred2()
- TestZ3. testBinderPred3()
- TestZ3. testDiv1()
- TestZ3. testDiv3()
- TestZ3. testDiv5()
- TestZ3. testDiv6()
- TestZ3. testEqual1()
- TestZ3. testEqual2()
- TestZ3. testEqui1()
- TestZ3. testEqui2()
- TestZ3. testImply()
- TestZ3. testImply2()
- TestZ3. testImply3()
- TestZ3. testLogicalIte1()
- TestZ3. testLogicalIte2()
- TestZ3. testOrnot()
- TestZ3. testSubsort1()
- TestZ3. testSubsort2()
- TestJMLPreTranslator. disabled_testMLCommentEndInSLComment1()
- TestJMLPreTranslator. disabled_testMLCommentEndInSLComment2()
- TestTriggersSet. testTrigger2()
- DesignTests. xtestTermSubclassVisibility()
- TestProofUserManager. testUserManagement_NoEnvironment()