if statements

Pi-Squared-Inc · Aug 26, 2024 · decce7d · decce7d
1 parent 00363a4
commit decce7d
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/src/solidity-syntax.md b/src/solidity-syntax.md
@@ -183,8 +183,8 @@ Following is a list of supported statements.
                                             | VariableDeclaration "=" Expression ";" [strict(2)]
                                             | "(" VariableDeclaration "," ")" "=" Expression ";" [strict(2)]
 
-    syntax IfStatement ::= "if" "(" Expression ")" Statement
-                         | "if" "(" Expression ")" Statement "else" Statement
+    syntax IfStatement ::= "if" "(" Expression ")" Statement [strict(1)]
+                         | "if" "(" Expression ")" Statement "else" Statement [avoid, strict(1)]
 
     syntax ForStatement ::= "for" "(" InitStatement ConditionStatement PostLoopStatement ")" Statement
     syntax InitStatement ::= VariableDeclarationStatement | ExpressionStatement | ";"

diff --git a/src/statement.md b/src/statement.md
@@ -31,4 +31,9 @@ module SOLIDITY-STATEMENT
        <events>... .List => ListItem(event(X, ARGS)) </events>
     requires isKResult(ARGS)
 
+  // if statement
+  rule if ( v(true, bool ) ) S => S
+  rule if ( v(false, bool ) ) _ => .K
+  rule if ( v(true, bool ) ) S else _ => S
+  rule if ( v(false, bool ) ) _ else S => S
 endmodule