MergeRuleTests

11

tests

0

failures

0

ignored

1m1.03s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 9.562s passed
testDoAutomaticGcdProofWithMergePointStatements() 9.195s passed
testDoManualGcdProof() 16.377s passed
testLoadClosedGcdProofWithMergePointStatements() 3.689s passed
testLoadGcdProof() 3.520s passed
testLoadGcdProofWithPredAbstr() 3.783s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.484s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.095s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.751s passed
testMergeIndistinguishablePathConditionsWithITE() 2.895s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.680s passed

Standard output

421804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
421804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.9ns 
421804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421906     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
421906     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
421906     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
421906     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
422291     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
425414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
425445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
425445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
438187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
438202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 629.1ns 
438202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
441032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
441282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 246.47ms 
441282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
441282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
441298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
444140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
444140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ns 
450844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
450844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.5ns 
450844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
453817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
454326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 475.74ms 
454329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
454329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
454331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
457366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
458109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 699.14ms 
458113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
458113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.8ns 
458115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
460784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
460784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 559.1ns 
460784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
460784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
460784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
463528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
463528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 415.6ns 
463543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
463543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 334.5ns 
463543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
466426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
467232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 761.73ms 
467248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
467248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.01ms 
467248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
470133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
470133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 438.1ns 
470133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
470133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.2ns 
470133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
472872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
472872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.2ns 
479322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
479322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 450.1ns 
479322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
482180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
482842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.38ms