MergeRuleTests

11

tests

0

failures

0

ignored

1m48.32s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 17.063s passed
testDoAutomaticGcdProofWithMergePointStatements() 17.180s passed
testDoManualGcdProof() 26.872s passed
testLoadClosedGcdProofWithMergePointStatements() 6.709s passed
testLoadGcdProof() 6.494s passed
testLoadGcdProofWithPredAbstr() 6.781s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.082s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.539s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.116s passed
testMergeIndistinguishablePathConditionsWithITE() 5.347s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.136s passed

Standard output

805793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
805793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 581.4ns 
805793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
806059     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
806059     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
806059     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
806059     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
806873     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
812478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.67s 
812525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
812525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
832663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
832663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 517.9ns 
832663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
837812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s 
837875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
838203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 307.64ms 
838203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
838203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
838203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
843564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.37s 
843626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
843642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.3ns 
855266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
855266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.1ns 
855266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
860552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.27s 
860599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
861348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 673.23ms 
861348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
861348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 557.2ns 
861363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
867015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.67s 
867078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
868129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 958.32ms 
868145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
868145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135ns 
868145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
873233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 
873265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
873265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 511.6ns 
873265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
873265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125ns 
873280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
878318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.05s 
878350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
878350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 444.4ns 
878381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
878381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.1ns 
878381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
883902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.53s 
883965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
885090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03s 
885090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
885105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.49ms 
885105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
890405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.31s 
890437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
890437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 343.8ns 
890437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
890437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 511.5ns 
890452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
896081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.64s 
896143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
896143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.9ns 
907664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
907664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.3ms 
907664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
913071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.41s 
913134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
914112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 892.22ms