MergeRuleTests

11

tests

0

failures

0

ignored

1m54.48s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 17.826s passed
testDoAutomaticGcdProofWithMergePointStatements() 18.442s passed
testDoManualGcdProof() 28.024s passed
testLoadClosedGcdProofWithMergePointStatements() 6.908s passed
testLoadGcdProof() 7.524s passed
testLoadGcdProofWithPredAbstr() 6.916s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.470s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 6.073s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.314s passed
testMergeIndistinguishablePathConditionsWithITE() 5.637s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.347s passed

Standard output

841163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
841179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.54ms 
841195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
841420     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
841420     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
841420     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
841420     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
842259     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
848324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.13s 
848387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
848387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 
869186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
869186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 630.5ns 
869201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
874771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.58s 
874833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
875260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 409.18ms 
875260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
875260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139ns 
875260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
881013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.76s 
881092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
881092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18ns 
893101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
893101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 558.8ns 
893101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
898756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.65s 
898818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
899557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.8ms 
899557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
899557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 506.3ns 
899557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
905367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.81s 
905429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
906473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 933.09ms 
906473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
906473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.8ns 
906489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
911789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.31s 
911820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
911820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 516.5ns 
911820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
911820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196ns 
911820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
917072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.25s 
917103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
917103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 322.3ns 
917134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
917134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 478.2ns 
917134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
922763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.63s 
922811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
924026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11s 
924042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
924042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.2ms 
924057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
929648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.59s 
929663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
929663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 349.4ns 
929679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
929679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 501.1ns 
929679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
935814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.14s 
935876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
935876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.1ns 
948121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
948121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 718.9ns 
948121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
954503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.38s 
954566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
955630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 860.02ms