MergeRuleTests

11

tests

0

failures

0

ignored

1m21.12s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.736s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.982s passed
testDoManualGcdProof() 21.908s passed
testLoadClosedGcdProofWithMergePointStatements() 4.849s passed
testLoadGcdProof() 4.884s passed
testLoadGcdProofWithPredAbstr() 4.799s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.371s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.003s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.372s passed
testMergeIndistinguishablePathConditionsWithITE() 3.669s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.544s passed

Standard output

532958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
532958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 483ns 
532958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533101     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
533101     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
533102     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
533102     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
533773     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
537340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.38s 
537387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
537387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
554873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
554873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 450.5ns 
554873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 
558533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
558877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 335.07ms 
558893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
558893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.2ns 
558893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
562376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
562376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.4ns 
571613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
571613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.1ns 
571613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
575158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
575984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 793.4ms 
575984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
575984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 435.8ns 
575984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 
579634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
580783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1s 
580799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
580799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.4ns 
580799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
584327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
584327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.7ns 
584327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
584327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
584327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
587668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
587668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 665.6ns 
587699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
587699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.9ns 
587699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
591267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
592533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24s 
592548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
592548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 428.4ns 
592548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
596217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
596217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595.7ns 
596217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
596217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.1ns 
596233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
599703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
599703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.9ns 
609199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
609199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 494.9ns 
609199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
612908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
614083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06s