MergeRuleTests

11

tests

0

failures

0

ignored

1m25.91s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.051s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.843s passed
testDoManualGcdProof() 25.205s passed
testLoadClosedGcdProofWithMergePointStatements() 5.042s passed
testLoadGcdProof() 4.160s passed
testLoadGcdProofWithPredAbstr() 4.091s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.145s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.703s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.316s passed
testMergeIndistinguishablePathConditionsWithITE() 3.160s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.190s passed

Standard output

540716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
540716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.9ns 
540716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540923     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
540923     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
540923     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
540923     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
541456     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
545226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.51s 
545273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
545273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ns 
565932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
565932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.2ns 
565932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
569361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
569619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 247.2ms 
569622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
569622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 615.8ns 
569626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
572993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
573009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.3ns 
584671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
584671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.7ns 
584671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
588215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
588800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 525.74ms 
588816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
588816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.5ns 
588816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
592183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
592907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 679.38ms 
592907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
592907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 424.2ns 
592923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
596097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
596097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 364.8ns 
596097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
596097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.5ns 
596097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
599382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
599398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 320.4ns 
599413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
599413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 669ns 
599429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 
603593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
604440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 799.03ms 
604455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
604455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.5ns 
604455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
607615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
607615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 235.2ns 
607615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
607615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.8ns 
607615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
610949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
610949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.3ns 
622458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
622458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427ns 
622458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
625953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
626618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 625.12ms