MergeRuleTests

11

tests

0

failures

0

ignored

1m41.68s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.914s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.263s passed
testDoManualGcdProof() 26.519s passed
testLoadClosedGcdProofWithMergePointStatements() 6.379s passed
testLoadGcdProof() 6.145s passed
testLoadGcdProofWithPredAbstr() 6.628s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.099s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.098s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.488s passed
testMergeIndistinguishablePathConditionsWithITE() 4.565s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.581s passed

Standard output

712460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
712460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.7ns 
712460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712648     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
712648     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
712648     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
712648     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
713524     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
718713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.25s 
718760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
718760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
738975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
738975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.5ns 
738975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
743714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
744073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 360.82ms 
744073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
744073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115ns 
744089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.69s 
748826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
748826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.9ns 
759987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
759987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.6ns 
759987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
764928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 
764975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
766086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05s 
766086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
766086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 519.5ns 
766101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.82s 
770963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
772714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66s 
772714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
772714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.3ns 
772714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
777264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.54s 
777279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
777295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
777295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
777295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.8ns 
777295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
781720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.43s 
781751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
781751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 809.7ns 
781783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
781783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.1ns 
781783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
786505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.73s 
786552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
788147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5s 
788162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
788162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.15ms 
788162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
792712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.54s 
792727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
792727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 722.3ns 
792727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
792727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.7ns 
792743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
797265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 
797312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
797312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15ns 
807990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
807990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.2ns 
807990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.6s 
812633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
814135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42s