HelloWorld Truffle test fix (#648)

* tests/truffle/HelloWorld: Fix HelloWorld test to run with ganache-cli * web3: Remove TAG handling from estimateGas for now * tests/failing.truffle: Remove HelloWorld from failing list * tests/truffle/HelloWorld/contracts/Migrations: Make consistent solidity version * web3: Create default block parameter for estimateGas * web3: Add default block for eth_call and fix eth_sign Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Jan 9, 2020 · 9931dc8 · 9931dc8
1 parent a12d133
commit 9931dc8
Show file tree

Hide file tree

Showing 6 changed files with 40 additions and 5 deletions.
diff --git a/tests/failing.truffle b/tests/failing.truffle
@@ -1,2 +1 @@
-tests/truffle/HelloWorld/truffle-config.js
 tests/truffle/openzeppelin-contracts/truffle-config.js
diff --git a/tests/truffle/HelloWorld/contracts/Migrations.sol b/tests/truffle/HelloWorld/contracts/Migrations.sol
@@ -0,0 +1,23 @@
+pragma solidity ^0.5.8;
+
+contract Migrations {
+  address public owner;
+  uint public last_completed_migration;
+
+  constructor() public {
+    owner = msg.sender;
+  }
+
+  modifier restricted() {
+    if (msg.sender == owner) _;
+  }
+
+  function setCompleted(uint completed) public restricted {
+    last_completed_migration = completed;
+  }
+
+  function upgrade(address new_address) public restricted {
+    Migrations upgraded = Migrations(new_address);
+    upgraded.setCompleted(last_completed_migration);
+  }
+}
diff --git a/tests/truffle/HelloWorld/migrations/1_initial_migration.js b/tests/truffle/HelloWorld/migrations/1_initial_migration.js
@@ -1,5 +1,5 @@
-var HelloWorld = artifacts.require("HelloWorld");
+const Migrations = artifacts.require("Migrations");
 
 module.exports = function(deployer) {
-    deployer.deploy(HelloWorld);
+  deployer.deploy(Migrations);
 };
diff --git a/tests/truffle/HelloWorld/migrations/2_deploy_contracts.js b/tests/truffle/HelloWorld/migrations/2_deploy_contracts.js
@@ -0,0 +1,5 @@
+var HelloWorld = artifacts.require("HelloWorld");
+
+module.exports = function(deployer) {
+    deployer.deploy(HelloWorld);
+};
diff --git a/tests/truffle/HelloWorld/test/HelloWorld.sol → ...ruffle/HelloWorld/test/TestHelloWorld.sol b/tests/truffle/HelloWorld/test/HelloWorld.sol → ...ruffle/HelloWorld/test/TestHelloWorld.sol
@@ -5,8 +5,10 @@ import "truffle/DeployedAddresses.sol";
 import "../contracts/HelloWorld.sol";
 
 contract TestHelloWorld {
+  string expected = "hello world";
+
   function testgetMessage() public {
     HelloWorld hw = HelloWorld(DeployedAddresses.HelloWorld());
-    Assert.equal("hello world", hw.getMessage(), "String should match");
+    Assert.equal(hw.getMessage(), expected, "String should match");
   }
 }
diff --git a/web3.md b/web3.md
@@ -448,7 +448,7 @@ WEB3 JSON RPC
 
     syntax KItem ::= "#eth_sign"
  // ----------------------------
-    rule <k> #eth_sign => #signMessage(KEY, #hashMessage(#unparseByteStack(#parseByteStack(MESSAGE)))) ... </k>
+    rule <k> #eth_sign => #signMessage(#unparseByteStack(#asByteStack(KEY)), #hashMessage(Hex2Raw(MESSAGE))) ... </k>
          <params> [ ACCTADDR, MESSAGE, .JSONs ] </params>
          <accountKeys>... #parseHexWord(ACCTADDR) |-> KEY ...</accountKeys>
 
@@ -1264,6 +1264,9 @@ Transaction Execution
 ```k
     syntax KItem ::= "#eth_call"
  // ----------------------------
+    rule <k> #eth_call ... </k>
+         <params> [ { _ }, (.JSONs => "pending", .JSONs) ] </params>
+
     rule <k> #eth_call
           => #pushNetworkState
           ~> #setMode NOGAS
@@ -1332,6 +1335,9 @@ Transaction Execution
 ```k
     syntax KItem ::= "#eth_estimateGas"
  // -----------------------------------
+    rule <k> #eth_estimateGas ... </k>
+         <params> [ { _ }, (.JSONs => "pending", .JSONs) ] </params>
+
     rule <k> #eth_estimateGas
           => #pushNetworkState
           ~> #loadTx J
Original file line number	Diff line number	Diff line change
		@@ -1,2 +1 @@
		tests/truffle/HelloWorld/truffle-config.js
		tests/truffle/openzeppelin-contracts/truffle-config.js