MergeRuleTests

11

tests

0

failures

0

ignored

59.841s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 9.530s passed
testDoAutomaticGcdProofWithMergePointStatements() 9.226s passed
testDoManualGcdProof() 15.861s passed
testLoadClosedGcdProofWithMergePointStatements() 3.810s passed
testLoadGcdProof() 3.517s passed
testLoadGcdProofWithPredAbstr() 3.733s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.292s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 2.906s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.703s passed
testMergeIndistinguishablePathConditionsWithITE() 2.615s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.648s passed

Standard output

425740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
425740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
425740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425837     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
425837     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
425837     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
425837     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
426237     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
429216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
429247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
429247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
441606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
441606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.9ns 
441606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
444296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
444515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 215.22ms 
444515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
444515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.1ns 
444515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
447312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
447328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.8ns 
454043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
454059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.1ns 
454059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
456833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
457336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 478.72ms 
457336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
457336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.5ns 
457336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
460327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
461069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 705.24ms 
461069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
461069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.8ns 
461069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
463708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
463723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 522.9ns 
463723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
463723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303ns 
463723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
466405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
466405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 431.3ns 
466421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
466421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.6ns 
466436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
469286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
470231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 913.68ms 
470231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
470231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.3ns 
470246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
472854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
472854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 371.4ns 
472854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
472854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns 
472854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
475558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
475573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.8ns 
482088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
482088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 523ns 
482088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
484917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
485589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.24ms