MergeRuleTests

11

tests

0

failures

0

ignored

1m36.70s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.981s passed
testDoAutomaticGcdProofWithMergePointStatements() 16.084s passed
testDoManualGcdProof() 28.390s passed
testLoadClosedGcdProofWithMergePointStatements() 5.533s passed
testLoadGcdProof() 5.136s passed
testLoadGcdProofWithPredAbstr() 5.883s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.622s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.107s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.476s passed
testMergeIndistinguishablePathConditionsWithITE() 3.770s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.715s passed

Standard output

583823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
583823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 808.2ns 
583823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583985     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
583985     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
583985     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
583985     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
584610     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
588828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5s 
588874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
588874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
612210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
612210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 488.3ns 
612210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 
615957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
616317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 350.4ms 
616317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
616317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
616317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s 
620589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
620589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.2ns 
632298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
632298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.7ns 
632298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
636029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
636920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 854.79ms 
636920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
636920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.2ns 
636920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.58s 
641549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
642803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2s 
642803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
642803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.6ns 
642803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s 
646518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
646518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 879.1ns 
646533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
646533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.2ns 
646533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
649978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
649978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 690.5ns 
650010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
650010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 594.3ns 
650010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 
653844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
655511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49s 
655527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
655527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.9ns 
655527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.74s 
659281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
659281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 665ns 
659297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
659297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 527.7ns 
659297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 
662968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
662968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.7ns 
675381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
675381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 529.6ns 
675381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 
679296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
680517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17s