MergeRuleTests

11

tests

0

failures

0

ignored

1m31.11s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.394s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.526s passed
testDoManualGcdProof() 25.397s passed
testLoadClosedGcdProofWithMergePointStatements() 5.179s passed
testLoadGcdProof() 4.839s passed
testLoadGcdProofWithPredAbstr() 5.102s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.697s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.027s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.547s passed
testMergeIndistinguishablePathConditionsWithITE() 3.777s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.625s passed

Standard output

564412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
564412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 542.9ns 
564412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564537     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
564537     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
564553     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
564553     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
565141     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
569259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s 
569306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
569321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
589820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
589820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 487.7ns 
589820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 
593495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
593833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 328.11ms 
593833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
593833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.4ns 
593833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s 
597655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
597655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.8ns 
609231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
609232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 500ns 
609235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s 
613055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
613909     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 829.82ms 
613925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
613925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.9ns 
613925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 
617857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
619027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12s 
619027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
619027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 513.1ns 
619043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
622652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
622652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 991.3ns 
622652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
622652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.9ns 
622668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
626164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
626164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 689.9ns 
626199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
626199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.6ns 
626199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.84s 
630078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
631363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24s 
631378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
631378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.89ms 
631378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.74s 
635139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
635155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 607.4ns 
635155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
635155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.5ns 
635155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 
638814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
638814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.7ns 
650681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
650681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.47ms 
650681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s 
654410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
655520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06s