preview of current formatting progress

CLIFlags/Helpers/Fibonacci.spec

@@ -2,13 +2,12 @@ methods {
     function fibonacci(uint32) external returns (uint32) envfree;
 }
 
-rule fibonacciMonotonicallyIncreasing {
+rule fibonacciMonotonicallyIncreasing() {
     uint32 i1;
     uint32 i2;
-
     assert i2 > i1 => fibonacci(i2) >= fibonacci(i1);
 }
 
-rule fifthFibonacciElementIsFive {
+rule fifthFibonacciElementIsFive() {
     assert fibonacci(5) == 5;
 }

CLIFlags/Helpers/auto_dispatcher/AutoDispatcherExample.spec

@@ -4,8 +4,7 @@ using E as e;
 rule r(uint n) {
     env environ;
     uint ret = foo(environ, n);
-
     assert currentContract.i == d || currentContract.i == e, "optimistic dispatching should promise this";
     assert currentContract.i == d => ret == n;
     assert currentContract.i == e => ret == n + 1;
-}
+}

CVLByExample/AddressFunctionCall/AddressCall.spec

@@ -1,7 +1,7 @@
 using A as a;
 using B as b;
 
-rule AddressCall {
+rule AddressCall() {
     env e;
     address x;
     assert x.foo(e) >= 1 && x.foo(e) <= 2;

CVLByExample/ConfInheritance/MainSpec.spec

@@ -5,7 +5,7 @@
  */
 
 methods {
-    function currentBid() external returns uint256 envfree; 
+    function currentBid() external returns (uint256) envfree;
 }
 
 /// @title Basic rules ////////////////////////////////////////////////////
@@ -20,7 +20,7 @@ methods {
 rule bidIncreasesAssets() {
     env e;
     require(e.msg.sender != currentContract);
-    require(e.msg.value > currentBid() );
+    require(e.msg.value > currentBid());
     uint256 balanceBefore = nativeBalances[currentContract];
     bid(e);
     assert nativeBalances[currentContract] > balanceBefore;
@@ -37,8 +37,8 @@ rule bidSuccessfullyExpectVacuous() {
     env e;
     uint256 balanceBefore = nativeBalances[currentContract];
     require(e.msg.sender != currentContract);
-    require(e.msg.value > 0 &&  e.msg.value > balanceBefore);
-    require (balanceBefore > 0);
+    require(e.msg.value > 0 && e.msg.value > balanceBefore);
+    require(balanceBefore > 0);
     bid(e);
     assert nativeBalances[currentContract] >= balanceBefore;
 }

CVLByExample/ContractAlias/ContractAlias.spec

@@ -1,8 +1,10 @@
 import "Imported.spec";
 
-methods { function A.Always1() internal returns (uint) => ALWAYS(2);}
+methods {
+    function A.Always1() internal returns (uint) => ALWAYS(2);
+}
 
-rule verifySummaryOnAlias(){
+rule verifySummaryOnAlias() {
     env e;
     assert 2 == Always1(e);
-}
+}

CVLByExample/ContractAlias/Imported.spec

@@ -1 +1 @@
-using ContractA as A;
+using ContractA as A;