diff --git a/src/solidity-syntax.md b/src/solidity-syntax.md
index 71a3205..61035bc 100644
--- a/src/solidity-syntax.md
+++ b/src/solidity-syntax.md
@@ -168,7 +168,7 @@ In each code block, various statments and nested blocks can be present.
| VariableDeclarationStatement
| ExpressionStatement
| IfStatement
- | WhileStatement
+ | ForStatement
| EmitStatement
| ReturnStatement
| RevertStatement
@@ -188,9 +188,10 @@ Following is a list of supported statements.
syntax IfStatement ::= "if" "(" Expression ")" Statement [strict(1)]
| "if" "(" Expression ")" Statement "else" Statement [avoid, strict(1)]
- syntax WhileStatement ::= "while" "(" Expression ")" Statement
- syntax Block ::= "for" "(" VariableDeclarationStatement Expression ";" Expression ")" Statement [function]
- rule for (Init Cond ; Post) Body => { Init while(Cond) { Body Post; } }
+ syntax ForStatement ::= "for" "(" InitStatement ConditionStatement PostLoopStatement ")" Statement
+ syntax InitStatement ::= VariableDeclarationStatement | ExpressionStatement | ";"
+ syntax ConditionStatement ::= ExpressionStatement | ";"
+ syntax PostLoopStatement ::= Expression | ""
syntax EmitStatement ::= "emit" Expression "(" CallArgumentList ")" ";" [strict(2)]
diff --git a/src/statement.md b/src/statement.md
index c26453e..37b2d7f 100644
--- a/src/statement.md
+++ b/src/statement.md
@@ -45,7 +45,4 @@ module SOLIDITY-STATEMENT
rule restoreEnv(E) => .K ...
_ => E
- // while statement
- rule while (Cond) Body => if (Cond) {Body while(Cond) Body} else {.Statements}
-
endmodule
diff --git a/test/regression/for.ref b/test/regression/for.ref
deleted file mode 100644
index e95ea60..0000000
--- a/test/regression/for.ref
+++ /dev/null
@@ -1,100 +0,0 @@
-
-
- .K
-
-
- ForTest
-
-
- .IfaceCellMap
-
-
-
-
- ForTest
-
-
- .Map
-
-
- .List
-
-
-
-
- constructor
-
-
- public
-
-
- .List
-
-
- .List
-
-
- .List
-
-
- .List
-
-
- uint256 x = 5 ; uint256 y = 0 ; { uint256 x = 0 ; while ( x < 10 ) { { y = y + 2 ; .Statements } x = x + 1 ; .Statements } .Statements } require ( y == 20 , "" , .TypedVals ) ; require ( x == 5 , "" , .TypedVals ) ; .Statements
-
-
-
-
- .ContractEventCellMap
-
-
-
-
-
- 1p160
-
-
- 0p256
-
-
- 1p160
-
-
- 2p160
-
-
- ForTest
-
-
- x |-> var ( 0 , uint256 )
- y |-> var ( 1 , uint256 )
-
-
- 0 |-> 5p256
- 1 |-> 20p256
- 2 |-> 10p256
-
-
- .List
-
-
-
-
- 2p160
-
-
- ForTest
-
-
- .Map
-
-
-
-
- .List
-
-
- 3p160
-
-
-
diff --git a/test/regression/for.sol b/test/regression/for.sol
deleted file mode 100644
index 81abc3c..0000000
--- a/test/regression/for.sol
+++ /dev/null
@@ -1,14 +0,0 @@
-pragma solidity ^0.8.24;
-
-contract ForTest {
-
- constructor() {
- uint x = 5;
- uint y = 0;
- for (uint x = 0; x < 10; x = x + 1) {
- y = y + 2;
- }
- require(y == 20, "");
- require(x == 5, "");
- }
-}
diff --git a/test/regression/for.txn b/test/regression/for.txn
deleted file mode 100644
index b324409..0000000
--- a/test/regression/for.txn
+++ /dev/null
@@ -1 +0,0 @@
-create(1, 0, ForTest, )
diff --git a/test/regression/function.ref b/test/regression/function.ref
index b6cee27..b27ccbc 100644
--- a/test/regression/function.ref
+++ b/test/regression/function.ref
@@ -987,7 +987,7 @@
.List
- { uint256 i ; while ( i < path . length - 1 ) { { address input = path [ i ] ; address output = path [ i + 1 ] ; address [ ] memory tokens = uniswapV2Library_sortTokens ( input , output , .TypedVals ) ; uint256 amountOut = amounts [ i + 1 ] ; uint256 amount0Out = input == tokens [ 0 ] ? uint256 ( 0 , .TypedVals ) : amountOut ; uint256 amount1Out = input == tokens [ 0 ] ? amountOut : uint256 ( 0 , .TypedVals ) ; address to = i < path . length - 2 ? uniswapV2Library_pairFor ( output , path [ i + 2 ] , .TypedVals ) : _to ; UniswapV2Pair ( uniswapV2Library_pairFor ( input , output , .TypedVals ) , .TypedVals ) . swap ( amount0Out , amount1Out , to , .TypedVals ) ; .Statements } i ++ ; .Statements } .Statements } .Statements
+ for ( uint256 i ; i < path . length - 1 ; i ++ ) { address input = path [ i ] ; address output = path [ i + 1 ] ; address [ ] memory tokens = uniswapV2Library_sortTokens ( input , output , .TypedVals ) ; uint256 amountOut = amounts [ i + 1 ] ; uint256 amount0Out = input == tokens [ 0 ] ? uint256 ( 0 , .TypedVals ) : amountOut ; uint256 amount1Out = input == tokens [ 0 ] ? amountOut : uint256 ( 0 , .TypedVals ) ; address to = i < path . length - 2 ? uniswapV2Library_pairFor ( output , path [ i + 2 ] , .TypedVals ) : _to ; UniswapV2Pair ( uniswapV2Library_pairFor ( input , output , .TypedVals ) , .TypedVals ) . swap ( amount0Out , amount1Out , to , .TypedVals ) ; .Statements } .Statements
@@ -1213,7 +1213,7 @@
ListItem ( amounts )
- require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ amounts . length - 1 ] = amountOut ; { uint256 i = path . length - 1 ; while ( i > 0 ) { { uint256 [ ] memory reserves = uniswapV2Library_getReserves ( path [ i - 1 ] , path [ i ] , .TypedVals ) ; amounts [ i - 1 ] = uniswapV2Library_getAmountIn ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } i -- ; .Statements } .Statements } .Statements
+ require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ amounts . length - 1 ] = amountOut ; for ( uint256 i = path . length - 1 ; i > 0 ; i -- ) { uint256 [ ] memory reserves = uniswapV2Library_getReserves ( path [ i - 1 ] , path [ i ] , .TypedVals ) ; amounts [ i - 1 ] = uniswapV2Library_getAmountIn ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } .Statements
@@ -1237,7 +1237,7 @@
ListItem ( amounts )
- require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ 0 ] = amountIn ; { uint256 i ; while ( i < path . length - 1 ) { { uint256 [ ] memory reserves = uniswapV2Library_getReserves ( path [ i ] , path [ i + 1 ] , .TypedVals ) ; amounts [ i + 1 ] = uniswapV2Library_getAmountOut ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } i ++ ; .Statements } .Statements } .Statements
+ require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ 0 ] = amountIn ; for ( uint256 i ; i < path . length - 1 ; i ++ ) { uint256 [ ] memory reserves = uniswapV2Library_getReserves ( path [ i ] , path [ i + 1 ] , .TypedVals ) ; amounts [ i + 1 ] = uniswapV2Library_getAmountOut ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } .Statements