MergeRuleTests

11

tests

0

failures

0

ignored

1m51.84s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 17.638s passed
testDoAutomaticGcdProofWithMergePointStatements() 16.708s passed
testDoManualGcdProof() 27.994s passed
testLoadClosedGcdProofWithMergePointStatements() 6.917s passed
testLoadGcdProof() 6.602s passed
testLoadGcdProofWithPredAbstr() 6.965s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.524s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 6.124s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.430s passed
testMergeIndistinguishablePathConditionsWithITE() 5.487s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.449s passed

Standard output

838485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
838485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 564.4ns 
838485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
838700     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
838700     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
838700     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
838700     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
839640     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
845572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.09s 
845635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
845635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ns 
866477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
866477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.1ns 
866477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
872226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.75s 
872288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
872601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314.75ms 
872601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
872601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
872616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
878363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.75s 
878426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
878426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ns 
890239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
890239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.7ns 
890255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
895955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.71s 
896028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
896763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.07ms 
896763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
896763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.9ns 
896763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
902656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.89s 
902718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
903728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 909.22ms 
903728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
903728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.1ns 
903728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
909146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.42s 
909177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
909177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 495.9ns 
909177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
909177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445ns 
909177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
914545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.37s 
914576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
914576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 454.2ns 
914607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
914607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 583.4ns 
914607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
920264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.65s 
920326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
921524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1s 
921524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
921540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.38ms 
921540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
926980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 
926996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
927011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 303.8ns 
927011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
927011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 461.4ns 
927011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
932409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.4s 
932456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
932456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ns 
943734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
943734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 689.3ns 
943734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
949270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.53s 
949317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
950321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 917.2ms