MergeRuleTests

11

tests

0

failures

0

ignored

1m35.07s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.647s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.662s passed
testDoManualGcdProof() 23.982s passed
testLoadClosedGcdProofWithMergePointStatements() 5.842s passed
testLoadGcdProof() 5.933s passed
testLoadGcdProofWithPredAbstr() 5.661s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.591s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.048s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.380s passed
testMergeIndistinguishablePathConditionsWithITE() 4.635s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.690s passed

Standard output

707757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
707757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.5ns 
707757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707947     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
707947     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
707948     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
707948     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
708635     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
713737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.98s 
713784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
713786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
731738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
731738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.4ns 
731739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s 
736549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
736784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 230.19ms 
736786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
736787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 472.2ns 
736788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
741497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s 
741548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
741550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15ns 
751433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
751434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 466.7ns 
751435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 
756373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
757020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584.97ms 
757024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
757025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.7ns 
757026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
761783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s 
761827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
762682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 765.73ms 
762686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
762686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.2ns 
762687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
767348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.66s 
767369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
767373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 390ns 
767375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
767375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.8ns 
767376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 
771729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
771731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 287ns 
771755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
771755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
771755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.81s 
776612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
777589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 889.45ms 
777597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
777597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
777597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
782207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.61s 
782228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
782230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 435.2ns 
782232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
782232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.9ns 
782233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
786939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s 
786989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
786990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.9ns 
796896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
796896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.1ns 
796897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
801836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.94s 
801881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
802823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 850.42ms