MergeRuleTests

11

tests

0

failures

0

ignored

1m14.95s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.401s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.908s passed
testDoManualGcdProof() 20.552s passed
testLoadClosedGcdProofWithMergePointStatements() 4.271s passed
testLoadGcdProof() 4.092s passed
testLoadGcdProofWithPredAbstr() 4.400s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.915s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.567s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.360s passed
testMergeIndistinguishablePathConditionsWithITE() 3.255s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.232s passed

Standard output

500934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
500934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.1ns 
500934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501055     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
501056     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
501057     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
501057     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
501564     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
505001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.07s 
505039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
505040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns 
521486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
521486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 
521487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
524840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
525051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 207.81ms 
525053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
525054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.5ns 
525054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
528279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
528281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.7ns 
537453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
537454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
537454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
540738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
541366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 603.22ms 
541368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
541368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
541369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
544879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
545766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 846.08ms 
545769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
545769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
545770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
548997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
548999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 590.4ns 
549000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
549001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
549001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
552339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
552341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 491.1ns 
552361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
552361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
552362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
555603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
556627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 985.68ms 
556632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
556632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
556632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
559884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
559885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 440.6ns 
559887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
559887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
559887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
562958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
562959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ns 
571795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
571795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143ns 
571796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
574974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
575885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 872.87ms