Fix JML spec of TPCC#payment

With the extra exception in the throws list, for some reason, a StackOverflowError is thrown at runtime.
ftsrg · Jul 30, 2023 · 10f89a4 · 10f89a4
1 parent 69d9e40
commit 10f89a4
Showing 1 changed file with 1 addition and 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
@@ -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