MergeRuleTests

11

tests

0

failures

0

ignored

1m24.68s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.836s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.117s passed
testDoManualGcdProof() 23.945s passed
testLoadClosedGcdProofWithMergePointStatements() 4.701s passed
testLoadGcdProof() 4.675s passed
testLoadGcdProofWithPredAbstr() 4.895s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.447s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.785s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.451s passed
testMergeIndistinguishablePathConditionsWithITE() 3.540s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.286s passed

Standard output

535161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
535162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.2ns 
535162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535311     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
535311     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
535312     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
535312     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
535910     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
539838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
539889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
539891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
559107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
559107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns 
559108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
562629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
562890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 257.59ms 
562892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
562892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
562896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
566307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
566309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.9ns 
576727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
576727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
576728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
580414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
581172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 718.2ms 
581177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
581177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.5ns 
581178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.75s 
584973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
586068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03s 
586071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
586071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
586072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
589352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
589355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 976.3ns 
589356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
589356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
589357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
592781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
592783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618.9ns 
592807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
592807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
592808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
596332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
597503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12s 
597509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
597509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
597510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
601045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
601048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 597.5ns 
601049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
601049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
601050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
604528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
604530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ns 
615166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
615166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
615167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 
618831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
619838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 958.23ms