MergeRuleTests

11

tests

0

failures

0

ignored

1m38.43s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.168s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.530s passed
testDoManualGcdProof() 26.871s passed
testLoadClosedGcdProofWithMergePointStatements() 5.651s passed
testLoadGcdProof() 5.629s passed
testLoadGcdProofWithPredAbstr() 5.490s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.049s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.051s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.296s passed
testMergeIndistinguishablePathConditionsWithITE() 4.395s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.301s passed

Standard output

707361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
707361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.6ns 
707361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707595     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
707595     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
707595     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
707595     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
708395     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
713652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.29s 
713714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
713714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 
734227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
734227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 282.9ns 
734227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
738891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.65s 
738938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
739276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 321.63ms 
739280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
739280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 442.8ns 
739283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.49s 
743824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
743824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.2ns 
755446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
755446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.1ns 
755446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
759825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.37s 
759871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
760495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 577.29ms 
760495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
760495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 896.4ns 
760510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.54s 
765094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
765985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 836.49ms 
766000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
766000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.3ns 
766000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
770255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.26s 
770286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
770286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 340.8ns 
770286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
770286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.35ms 
770302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
774535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 
774567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
774567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 410.5ns 
774598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
774598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.7ns 
774598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.36s 
779105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
780233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05s 
780233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
780233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.9ns 
780233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
784613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.37s 
784628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
784628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 322.7ns 
784628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
784628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.6ns 
784644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
788794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.15s 
788841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
788857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.8ns 
800158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
800158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.8ns 
800158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
804724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.56s 
804771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
805772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 936.17ms