addresses can hold and receive ether

examples/solidity/basic/balance.sol

@@ -0,0 +1,11 @@
+contract C {
+  constructor() public {
+      //msg.sender.transfer(0);
+  }
+
+  function f() public {}
+  function echidna_balance() public returns (bool) { 
+      return address(msg.sender) == address(0x1) && msg.sender.balance == 42; 
+  }
+
+}

examples/solidity/basic/balance.yaml

@@ -0,0 +1,3 @@
+sender: ["0x1"]
+psender: "0x1"
+initialBalance: 42

examples/solidity/basic/default.yaml

@@ -9,6 +9,7 @@ shrinkLimit: 5000
 contractAddr: "0x00a329c0648769a73afac7f9381e08fb43dbea72"
 deployer: "0x00a329c0648769a73afac7f9381e08fb43dbea70"
 sender: ["0x00a329c0648769a73afac7f9381e08fb43dbea70"]
+initialBalance: 0xffffffff
 psender: "0x00a329c0648769a73afac7f9381e08fb43dbea70"
 prefix: "echidna_"
 solcArgs: ""

lib/Echidna/Config.hs

@@ -73,6 +73,7 @@ instance FromJSON EConfig where
             <*> (SolConf <$> v .:? "contractAddr"   .!= 0x00a329c0648769a73afac7f9381e08fb43dbea72
                          <*> v .:? "deployer"       .!= 0x00a329c0648769a73afac7f9381e08fb43dbea70
                          <*> v .:? "sender"         .!= [0x00a329c0648769a73afac7f9381e08fb43dbea70]
+                         <*> v .:? "initialBalance" .!= 0xffffffff
                          <*> v .:? "prefix"         .!= "echidna_"
                          <*> v .:? "solcArgs"       .!= ""
                          <*> v .:? "quiet"          .!= False)

lib/Echidna/Exec.hs

@@ -31,6 +31,7 @@ data ErrorClass = RevertE | IllegalE | UnknownE
 classifyError :: Error -> ErrorClass
 classifyError (Revert _)             = RevertE
 classifyError (UnrecognizedOpcode _) = RevertE
+classifyError (Query _)              = RevertE
 classifyError StackUnderrun          = IllegalE
 classifyError BadJumpDestination     = IllegalE
 classifyError StackLimitExceeded     = IllegalE

lib/Echidna/Solidity.hs

@@ -34,10 +34,12 @@ import Echidna.Exec        (execTx)
 import Echidna.Transaction (Tx(..), World(..))
 
 import EVM hiding (contracts)
+import qualified EVM (contracts)
 import EVM.ABI      (AbiValue(..))
 import EVM.Exec     (vmForEthrunCreation)
 import EVM.Solidity
 import EVM.Types    (Addr)
+import EVM.Concrete (w256)
 
 import qualified Data.ByteString     as BS
 import qualified Data.HashMap.Strict as M
@@ -73,6 +75,7 @@ instance Exception SolException
 data SolConf = SolConf { _contractAddr    :: Addr    -- ^ Contract address to use
                        , _deployer        :: Addr    -- ^ Contract deployer address to use
                        , _sender          :: [Addr]  -- ^ Sender addresses to use
+                       , _initialBalance  :: Integer -- ^ Initial balance of deployer and senders
                        , _prefix          :: Text    -- ^ Function name prefix used to denote tests
                        , _solcArgs        :: String  -- ^ Args to pass to @solc@
                        , _quiet           :: Bool    -- ^ Suppress @solc@ output, errors, and warnings
@@ -94,6 +97,12 @@ contracts fp = do
         readSolc =<< writeSystemTempFile ""
                  =<< readCreateProcess (proc "solc" $ usual <> words a) {std_err = stderr} ""
 
+populateAddresses :: [Addr] -> Integer -> VM -> VM
+populateAddresses []     _ vm = vm
+populateAddresses (a:as) b vm = populateAddresses as b (vm & set (env . EVM.contracts . at a) (Just account))
+                                 where account = initialContract mempty & set nonce 1 & set balance (w256 $ fromInteger b)
+
+
 -- | Given an optional contract name and a list of 'SolcContract's, try to load the specified
 -- contract, or, if not provided, the first contract in the list, into a 'VM' usable for Echidna
 -- testing and extract an ABI and list of tests. Throws exceptions if anything returned doesn't look
@@ -111,9 +120,9 @@ loadSpecified name cs = let ensure l e = if l == mempty then throwM e else pure
     unless q . putStrLn $ "Analyzing contract: " <> unpack (c ^. contractName)
 
   -- Local variables
-  (SolConf ca d _ pref _ _) <- view hasLens
+  (SolConf ca d ads b pref _ _) <- view hasLens
   let bc = c ^. creationCode
-      blank = vmForEthrunCreation bc
+      blank = populateAddresses (ads++[d]) b (vmForEthrunCreation bc)
       abi = liftM2 (,) (view methodName) (fmap snd . view methodInputs) <$> toList (c ^. abiMap)
       (tests, funs) = partition (isPrefixOf pref . fst) abi
 

src/test/Spec.hs

@@ -101,6 +101,9 @@ integrationTests = testGroup "Solidity Integration Testing"
       [ ("echidna_state failed",                  not . solved "echidna_state") ]
   , testContract "coverage/multi.sol"        Nothing
       [ ("echidna_state3 failed",                  not . solved "echidna_state3") ]
+  , testContract "basic/balance.sol"        (Just "basic/balance.yaml")
+      [ ("echidna_balance failed",                  passed       "echidna_balance") ]
+
   ]
 
 testContract :: FilePath -> Maybe FilePath -> [(String, Campaign -> Bool)] -> TestTree