MergeRuleTests

11

tests

0

failures

0

ignored

1m43.16s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 17.113s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.801s passed
testDoManualGcdProof() 26.796s passed
testLoadClosedGcdProofWithMergePointStatements() 6.375s passed
testLoadGcdProof() 5.816s passed
testLoadGcdProofWithPredAbstr() 6.160s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.869s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.251s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.733s passed
testMergeIndistinguishablePathConditionsWithITE() 4.385s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.857s passed

Standard output

736762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
736762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.5ns 
736762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
737029     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
737029     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
737029     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
737029     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
737771     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
742862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.1s 
742909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
742924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
763566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
763566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 541ns 
763566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
768381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.82s 
768444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
768803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 344.86ms 
768803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
768803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148ns 
768803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s 
773874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
773890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.6ns 
785916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
785916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.3ns 
785916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
790930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s 
791003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
791769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 717.96ms 
791785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
791785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 495.4ns 
791785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
796801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.02s 
796863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
797945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 988.81ms 
797945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
797945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 515.4ns 
797945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
802770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.83s 
802802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
802802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 497.5ns 
802802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
802802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.4ns 
802817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
807482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.67s 
807504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
807504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 397.8ns 
807550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
807550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 579ns 
807550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.92s 
812522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
813895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3s 
814036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
814036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.4ns 
814036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
818414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.37s 
818429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
818429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 351.1ns 
818445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
818445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.9ns 
818445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
823076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.64s 
823131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
823131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ns 
834230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
834230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 601.8ns 
834230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
838976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.75s 
839023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
840031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 938.63ms