MergeRuleTests

11

tests

0

failures

0

ignored

1m38.62s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.576s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.295s passed
testDoManualGcdProof() 24.668s passed
testLoadClosedGcdProofWithMergePointStatements() 6.354s passed
testLoadGcdProof() 5.532s passed
testLoadGcdProofWithPredAbstr() 6.277s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.929s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.238s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.565s passed
testMergeIndistinguishablePathConditionsWithITE() 4.659s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.527s passed

Standard output

681623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
681624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
681624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681781     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
681781     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
681781     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
681781     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
682485     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
687615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.99s 
687661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
687663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
706292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
706292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.1ns 
706293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
710971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
711056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
711526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 450.08ms 
711529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
711529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.1ns 
711536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.82s 
716430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
716432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.9ns 
727105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
727105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.1ns 
727106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
732012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 
732058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
733030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 723ms 
733034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
733035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 615ns 
733036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
737944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 
738031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
739307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11s 
739312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
739312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.8ns 
739313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.48s 
743822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
743831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 590.4ns 
743839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
743839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.1ns 
743840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.51s 
748376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
748378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314.1ns 
748403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
748403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.5ns 
748404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
753353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 
753398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
754736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13s 
754757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
754757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122ns 
754757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
759389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.63s 
759411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
759414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 327.8ns 
759417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
759417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.9ns 
759418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
764170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.75s 
764215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
764217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.6ns 
774713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
774713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.9ns 
774714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 
779288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
780239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.5ms