Fix markdown text; remove infiniteGas in tests

runtimeverification · Jul 25, 2023 · b433541 · b433541
1 parent 3ea7732
commit b433541
Show file tree

Hide file tree

Showing 6 changed files with 4 additions and 11 deletions.
diff --git a/include/kframework/foundry.md b/include/kframework/foundry.md
@@ -906,7 +906,8 @@ function setGas(uint256 newGas) external;
 function infiniteGas() external;
 ```
 
-`infiniteGas` is useful for running tests without them running out of gas. It is applied by default.
+`infiniteGas` is useful for running tests without them running out of gas.
+It is applied by default.
 
 ```{.k .bytes .symbolic}
     rule [foundry.call.infiniteGas]:

diff --git a/kevm-pyk/src/tests/integration/test-data/foundry/test/CounterTest.t.sol b/kevm-pyk/src/tests/integration/test-data/foundry/test/CounterTest.t.sol
@@ -25,7 +25,6 @@ contract CounterTest is Test, KEVMCheats {
     // }
 
     function testIncrement() public {
-        kevm.infiniteGas();
         counter = new Counter();
         counter.setNumber(0);
         counter.increment();
@@ -34,7 +33,6 @@ contract CounterTest is Test, KEVMCheats {
 
     function testSetNumber(uint256 x) public {
         //setUp();
-        kevm.infiniteGas();
         counter = new Counter();
         counter.setNumber(0);
         counter.setNumber(x);

diff --git a/kevm-pyk/src/tests/integration/test-data/foundry/test/GasTest.t.sol b/kevm-pyk/src/tests/integration/test-data/foundry/test/GasTest.t.sol
@@ -6,7 +6,7 @@ import "../src/KEVMCheats.sol";
 
 contract GasTest is Test, KEVMCheats {
     function testInfiniteGas() public {
-        kevm.infiniteGas();
+        // Infinite gas is used by default
         uint256 gasLeftBefore = gasleft();
         uint256 x = 345;
         uint256 y = 928;

diff --git a/tests/foundry/test/CounterTest.t.sol b/tests/foundry/test/CounterTest.t.sol
@@ -25,7 +25,6 @@ contract CounterTest is Test, KEVMCheats {
     // }
 
     function testIncrement() public {
-        kevm.infiniteGas();
         counter = new Counter();
         counter.setNumber(0);
         counter.increment();
@@ -34,7 +33,6 @@ contract CounterTest is Test, KEVMCheats {
 
     function testSetNumber(uint256 x) public {
         //setUp();
-        kevm.infiniteGas();
         counter = new Counter();
         counter.setNumber(0);
         counter.setNumber(x);

diff --git a/tests/foundry/test/FreshInt.t.sol b/tests/foundry/test/FreshInt.t.sol
@@ -9,28 +9,24 @@ contract FreshIntTest is Test, KEVMCheats {
     int128 constant max = 170141183460469231731687303715884105727;
 
     function test_uint128() public {
-        kevm.infiniteGas();
         uint256 fresh_uint128 = uint256(kevm.freshUInt(32));
         assertGe(fresh_uint128, type(uint128).min);
         assertLe(fresh_uint128, type(uint128).max);
     }
 
     function test_bool() public {
-        kevm.infiniteGas();
         uint256 fresh_uint256 = kevm.freshBool();
         assertGe(fresh_uint256, 0);
         assertLe(fresh_uint256, 1);
     }
 
     function test_int128() public {
-        kevm.infiniteGas();
         int128 val = int128(uint128(kevm.freshUInt(16)));
         assertGe(val, min);
         assertLe(val, max);
     }
 
     function testFail_int128() public {
-        kevm.infiniteGas();
         int128 val = int128(uint128(kevm.freshUInt(16)));
         assertGt(val, max);
     }

diff --git a/tests/foundry/test/GasTest.t.sol b/tests/foundry/test/GasTest.t.sol
@@ -6,7 +6,7 @@ import "../src/KEVMCheats.sol";
 
 contract GasTest is Test, KEVMCheats {
     function testInfiniteGas() public {
-        kevm.infiniteGas();
+        // Infinite gas is used by default
         uint256 gasLeftBefore = gasleft();
         uint256 x = 345;
         uint256 y = 928;