MergeRuleTests

11

tests

0

failures

0

ignored

1m34.34s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.262s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.509s passed
testDoManualGcdProof() 27.019s passed
testLoadClosedGcdProofWithMergePointStatements() 5.268s passed
testLoadGcdProof() 5.096s passed
testLoadGcdProofWithPredAbstr() 5.441s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.862s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.159s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.440s passed
testMergeIndistinguishablePathConditionsWithITE() 3.643s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.642s passed

Standard output

551337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
551337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 527ns 
551337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551494     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
551494     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
551494     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
551494     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
552307     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
556248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 
556311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
556311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11ns 
578354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
578354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.1ns 
578354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 
582153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
582513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 355.47ms 
582513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
582513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.7ns 
582513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s 
586360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
586360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.3ns 
598775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
598775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.9ns 
598775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.82s 
602668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
603637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 920.08ms 
603653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
603653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.1ns 
603653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 
607624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
609062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37s 
609078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
609078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 401ns 
609078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
612705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
612705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
612720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
612720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.3ns 
612720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s 
616144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
616144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 866.4ns 
616175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
616175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.5ns 
616175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 
619927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
621412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43s 
621428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
621428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.4ns 
621428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 
625071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
625071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 962.5ns 
625071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
625071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 433.6ns 
625086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
628650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
628650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ns 
640580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
640580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 466.9ns 
640595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.72s 
644363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
645676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26s