Skip to content

Commit

Permalink
test: remove constant
Browse files Browse the repository at this point in the history
  • Loading branch information
zoep committed Nov 7, 2023
1 parent 2d10fbe commit 9d93ad5
Showing 1 changed file with 0 additions and 17 deletions.
17 changes: 0 additions & 17 deletions tests/coq/ERC20/erc20.act
Original file line number Diff line number Diff line change
Expand Up @@ -28,11 +28,6 @@ case CALLER =/= to:

case CALLER == to:

storage

balanceOf[CALLER]
balanceOf[to]

returns 1


Expand All @@ -50,8 +45,6 @@ case src =/= dst and CALLER == src:

storage

balanceOf[CALLER]
allowance[src][CALLER]
balanceOf[src] => balanceOf[src] - amount
balanceOf[dst] => balanceOf[dst] + amount

Expand All @@ -61,8 +54,6 @@ case src =/= dst and CALLER =/= src and allowance[src][CALLER] == 2^256 - 1:

storage

balanceOf[CALLER]
allowance[src][CALLER]
balanceOf[src] => balanceOf[src] - amount
balanceOf[dst] => balanceOf[dst] + amount

Expand All @@ -72,7 +63,6 @@ case src =/= dst and CALLER =/= src and allowance[src][CALLER] < 2^256 - 1:

storage

balanceOf[CALLER]
allowance[src][CALLER] => allowance[src][CALLER] - amount
balanceOf[src] => balanceOf[src] - amount
balanceOf[dst] => balanceOf[dst] + amount
Expand All @@ -81,11 +71,4 @@ case src =/= dst and CALLER =/= src and allowance[src][CALLER] < 2^256 - 1:

case src == dst:

storage

balanceOf[CALLER]
allowance[src][CALLER]
balanceOf[src]
balanceOf[dst]

returns 1

0 comments on commit 9d93ad5

Please sign in to comment.