MergeRuleTests

11

tests

0

failures

0

ignored

1m22.81s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.135s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.372s passed
testDoManualGcdProof() 22.559s passed
testLoadClosedGcdProofWithMergePointStatements() 4.484s passed
testLoadGcdProof() 4.477s passed
testLoadGcdProofWithPredAbstr() 4.422s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.086s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.720s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.167s passed
testMergeIndistinguishablePathConditionsWithITE() 3.545s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.844s passed

Standard output

516022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
516022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 842.2ns 
516022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516140     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
516140     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
516140     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
516140     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
516804     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
520804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.77s 
520835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
520850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
538573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
538573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 504.2ns 
538573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
541966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
542293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 320.64ms 
542293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
542293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.1ns 
542309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
545646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
545646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17ns 
556459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
556459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.4ns 
556459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
559824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
560500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 655.68ms 
560515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
560515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.6ns 
560515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
563968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
564922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 905.55ms 
564937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
564937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.9ns 
564937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.81s 
568765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
568781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 833.7ns 
568781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
568781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.3ns 
568781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
571916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
571932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 569.7ns 
571948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
571948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 455.7ns 
571948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
575361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
576417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01s 
576432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
576432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 455.3ns 
576432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
579899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
579962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 897.7ns 
579977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
579977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 485.9ns 
579993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 
584111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
584111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.9ns 
594361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
594361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.7ns 
594361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
597921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
598838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 879.32ms