rename G => GAAS in one of the lemmas. (#433)

runtimeverification · Aug 13, 2019 · b31f51b · b31f51b
1 parent 615db59
commit b31f51b
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 9 deletions.
diff --git a/tests/specs/ds-token-erc20/abstract-semantics-segmented-gas.k b/tests/specs/ds-token-erc20/abstract-semantics-segmented-gas.k
@@ -15,10 +15,10 @@ module ABSTRACT-SEMANTICS-SEGMENTED-GAS
   // ########################
 
   // accumulate the gas cost and never run out of gas
-  rule <k> G ~> #deductGas => . ... </k>
-       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
+  rule <k> GAAS:Int ~> #deductGas => . ... </k>
+       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int GAAS, MEM) </gas>
        <callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
-    requires #notKLabel(G, "#symCmem")
+    requires #notKLabel(GAAS, "#symCmem")
     [trusted, matching(#gas)]
 
   rule <k> #symCmem(MEM') ~> #deductGas => . ... </k>

diff --git a/tests/specs/hkg-erc20/abstract-semantics-segmented-gas.k b/tests/specs/hkg-erc20/abstract-semantics-segmented-gas.k
@@ -15,10 +15,10 @@ module ABSTRACT-SEMANTICS-SEGMENTED-GAS
   // ########################
 
   // accumulate the gas cost and never run out of gas
-  rule <k> G ~> #deductGas => . ... </k>
-       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
+  rule <k> GAAS:Int ~> #deductGas => . ... </k>
+       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int GAAS, MEM) </gas>
        <callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
-    requires #notKLabel(G, "#symCmem")
+    requires #notKLabel(GAAS, "#symCmem")
     [trusted, matching(#gas)]
 
   rule <k> #symCmem(MEM') ~> #deductGas => . ... </k>

diff --git a/tests/specs/hobby-erc20/abstract-semantics-segmented-gas.k b/tests/specs/hobby-erc20/abstract-semantics-segmented-gas.k
@@ -15,10 +15,10 @@ module ABSTRACT-SEMANTICS-SEGMENTED-GAS
   // ########################
 
   // accumulate the gas cost and never run out of gas
-  rule <k> G ~> #deductGas => . ... </k>
-       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int G, MEM) </gas>
+  rule <k> GAAS:Int ~> #deductGas => . ... </k>
+       <gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int GAAS, MEM) </gas>
        <callGas> _ => #gas(INITGAS, NONMEM, MEM) </callGas>
-    requires #notKLabel(G, "#symCmem")
+    requires #notKLabel(GAAS, "#symCmem")
     [trusted, matching(#gas)]
 
   rule <k> #symCmem(MEM') ~> #deductGas => . ... </k>