MergeRuleTests

11

tests

0

failures

0

ignored

1m21.62s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.138s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.200s passed
testDoManualGcdProof() 24.105s passed
testLoadClosedGcdProofWithMergePointStatements() 4.234s passed
testLoadGcdProof() 4.049s passed
testLoadGcdProofWithPredAbstr() 4.555s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.885s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.629s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.129s passed
testMergeIndistinguishablePathConditionsWithITE() 3.331s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.360s passed

Standard output

510043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
510043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.7ns 
510043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510153     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
510153     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
510153     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
510153     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
510658     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
514394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 
514441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
514441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
534142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
534158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 502.9ns 
534158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
537471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
537770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 284.59ms 
537772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
537772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.7ns 
537775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
541332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
541364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.9ns 
551909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
551909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.8ns 
551924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
555290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
555794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 462.3ms 
555794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
555794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.7ns 
555794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 
559610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
560349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.08ms 
560349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
560349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.2ns 
560349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
563709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
563709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 381.9ns 
563709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
563709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.5ns 
563724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
566807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
566822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 256.7ns 
566853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
566853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 487.1ns 
566853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
570254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
571056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 763.23ms 
571072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
571072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 676.6ns 
571072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
574388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
574388     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 282ns 
574403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
574403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.5ns 
574403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
577761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
577761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.2ns 
587603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
587603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 501.4ns 
587603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
591058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
591652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 541.42ms