From 10f89a407b60f0fd771e78ce310d4874aa326544 Mon Sep 17 00:00:00 2001 From: bzp99 Date: Sun, 30 Jul 2023 11:12:40 +0200 Subject: [PATCH] Fix JML spec of TPCC#payment With the extra exception in the throws list, for some reason, a StackOverflowError is thrown at runtime. --- .../v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/TPCC.jml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/TPCC.jml b/smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/TPCC.jml index 3485de8..7f62c44 100644 --- a/smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/TPCC.jml +++ b/smart-contract/hyperledger-fabric/v2/java/specs/hu/bme/mit/ftsrg/chaincode/tpcc/TPCC.jml @@ -19,7 +19,7 @@ public final class TPCC implements ContractInterface { @ ensures \result.getSkipped() == 10 - \result.getDelivered().size(); // C.TXIO:DELIVERY:FORM_SKIPPED @*/ private DeliveryOutput delivery(final TPCCContext ctx, final DeliveryInput input) - throws EntityNotFoundException, EntityExistsException; + throws EntityNotFoundException; /*@ @ ensures \result.getW_id() == input.getW_id(); // C.TXIO:NEWORDER:EQ_W_ID