MergeRuleTests

11

tests

0

failures

0

ignored

1m8.93s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.507s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.213s passed
testDoManualGcdProof() 19.079s passed
testLoadClosedGcdProofWithMergePointStatements() 4.111s passed
testLoadGcdProof() 3.757s passed
testLoadGcdProofWithPredAbstr() 3.960s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.607s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.181s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.892s passed
testMergeIndistinguishablePathConditionsWithITE() 2.830s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.789s passed

Standard output

438636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
438636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 431.5ns 
438636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438749     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
438749     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
438749     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
438749     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
439203     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
442370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.72s 
442402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
442402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
457708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
457708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 477.8ns 
457723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
460609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
460890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 272.33ms 
460890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
460890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.8ns 
460890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
463871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
463871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.7ns 
472397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
472397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 466.7ns 
472397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
475428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
476005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 544.57ms 
476005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
476005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.8ns 
476005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
479134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
479950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 778.61ms 
479965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
479965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.3ns 
479965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
482744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
482744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 769.3ns 
482744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
482744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.62ms 
482760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
485616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
485631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 612.5ns 
485647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
485647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 403ns 
485647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
488648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
489758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08s 
489774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
489774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.42ms 
489774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
492595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
492595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 503.5ns 
492595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
492595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.1ns 
492595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
495434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
495434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.1ns 
503803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
503803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 580.7ns 
503803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
506810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
507545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 715.11ms