Echidna（Fuzz）关于发送以太币的断言测试失败

Question

我目前正在使用 Echidna 测试断言。

[测试文件]

contract ReceiveEther {

    constructor() payable {}

    function receiveEther() public payable {
        uint256 amount = msg.value;
        assert(address(this).balance == amount);
    }
}

[yaml]

maxValue: 100000000000000000000 #100 eth
balanceContract: 0

[测试命令]

echidna-test --config ./echidna.yaml ./ReceiveEther.sol --contract ReceiveEther --测试模式断言

[结果]

receiveEther(): failed!💥  
  Call sequence:
    receiveEther() Value: 0x1
    receiveEther()

Event sequence: Panic(1)

测试结果预计会通过。但由于某种原因
模糊测试没有像上面的日志那样通过。

我不知道为什么以下行在 Echidna 中没有通过：

assert(地址(this).余额==金额);

如果有人知道原因请告诉我。

Answer 1

我想我能够重现您的错误并添加一些要记录的事件，以便更清楚发生了什么。

所以一步一步：

• receiveEther 被调用，msg.value 为 1
  • 消息值=1
  • 地址（这个）.余额= 1
  • assert(1 = 1) - 每个人都很高兴函数结束
• echinda 再次调用该函数，但这次没有 msg.value，所以基本上为 0。
  • 消息值=0
  • address(this).balance = 1（合约会记住 - 从第一次调用开始）
  • assert (0 = 1) - 哎呀，这看起来不对

你可以查看打印的痕迹，这应该是第二次调用失败的结果。余额 = 1，而消息值 = 0。

稍微修改了代码：

contract ReceiveEther {

    constructor() payable {}

    event Balance(uint256 balance);
    event MsgValue(uint256 value);

    function receiveEther() public payable {
        uint256 amount = msg.value;
        emit Balance(address(this).balance);
        emit MsgValue(msg.value);
        assert(address(this).balance == amount);
    }
}

针鼹输出：

assertion in receiveEther(): FAILED! with ErrorRevert                                              ^│
│                                                                                                     │
│ Call sequence:                                                                                      │
│ 1. ReceiveEther.receiveEther() Value: 0x1                                                           │
│ 2. ReceiveEther.receiveEther()                                                                      │
│                                                                                                     │
│ Traces:                                                                                             │
│ Balance(balance=1) (/home/bingbong/iliketrains/echidnaReceiveEth/Receive.sol:10) 
│ MsgValue(value=0) (/home/bingbong/iliketrains/echidnaReceiveEth/Receive.sol:11)