Make checkNoPayment work in symbolic execution (#115)

runtimeverification · Jul 15, 2023 · dd6bbf3 · dd6bbf3
1 parent 99e92e2
commit dd6bbf3
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/vmhooks/baseOps.md b/vmhooks/baseOps.md
@@ -209,8 +209,8 @@ module BASEOPS
     rule [checkNoPayment-pass]:
         <instrs> hostCall("env", "checkNoPayment", [ .ValTypes ] -> [ .ValTypes ]) => . ... </instrs>
         <callValue> VAL </callValue>
-        <esdtTransfers> .List </esdtTransfers>
-      requires VAL <=Int 0
+        <esdtTransfers> T:List </esdtTransfers>
+      requires VAL <=Int 0 andBool size(T) ==K 0
 
     rule [checkNoPayment-fail-egld]:
         <instrs> hostCall("env", "checkNoPayment", [ .ValTypes ] -> [ .ValTypes ]) 
@@ -224,8 +224,8 @@ module BASEOPS
               => #throwException(ExecutionFailed, "function does not accept ESDT payment") ... 
         </instrs>
         <callValue> VAL </callValue>
-        <esdtTransfers> ListItem(_) ... </esdtTransfers>
-      requires VAL <=Int 0
+        <esdtTransfers> T:List </esdtTransfers>
+      requires VAL <=Int 0 andBool 0 <Int size(T)
 
     // extern int32_t getESDTTokenName(void *context, int32_t resultOffset);
     rule [getESDTTokenName]: