runtimeverification / ercx-vscode

VSCode support for ERCx
BSD 3-Clause "New" or "Revised" License
1 stars 1 forks source link

Tests on the extension run indefinitely #28

Open ACassimiro opened 11 months ago

ACassimiro commented 11 months ago

I’ve been doing some testing with ERCx’s VSCode extension and I’m noticing what seems to be some usability issues, mainly regarding the handling of possible errors in the communication with the API. One example is a set of tests that I’m running on a simple ERC20 contract, which the IDE claims has been running for almost 14 hours (as seen in the image below).

image

Code in which the tests were applied to:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.14;

interface IERC20 {

    function totalSupply() external view returns (uint256);
    function balanceOf(address account) external view returns (uint256);
    function allowance(address owner, address spender) external view returns (uint256);

    function transfer(address recipient, uint256 amount) external returns (bool);
    function approve(address spender, uint256 amount) external returns (bool);
    function transferFrom(address sender, address recipient, uint256 amount) external returns (bool);

    event Transfer(address indexed from, address indexed to, uint256 value);
    event Approval(address indexed owner, address indexed spender, uint256 value);
}

contract SalchainToken is IERC20 {
    using SafeMath for uint256;

    string  public  name;
    string  public  symbol;
    uint8   public  decimals;
    uint256 public  totalSupply_;

    mapping(address => uint256) balances;
    mapping(address => mapping (address => uint256)) allowed;

    constructor()  {
        name = "Salchain1";
        symbol = "SAL";
        decimals = 10;
        totalSupply_ = 1000000000000;     // total tokens would equal (totalSupply_/10**decimals)=1000
        balances[msg.sender] = totalSupply_;
    }

    function totalSupply() public override view returns (uint256) {
        return totalSupply_;
    }

    function balanceOf(address tokenOwner) public override view returns (uint256) {
        return balances[tokenOwner];
    }

    function transfer(address receiver, uint256 numTokens) public override returns (bool) {
        require(numTokens <= balances[msg.sender]);
        balances[msg.sender] = balances[msg.sender].sub(numTokens);
        balances[receiver] = balances[receiver].add(numTokens);
        emit Transfer(msg.sender, receiver, numTokens);
        return true;
    }

    function approve(address delegate, uint256 numTokens) public override returns (bool) {
        allowed[msg.sender][delegate] = numTokens;
        emit Approval(msg.sender, delegate, numTokens);
        return true;
    }

    function allowance(address owner, address delegate) public override view returns (uint) {
        return allowed[owner][delegate];
    }

    function transferFrom(address owner, address buyer, uint256 numTokens) public override returns (bool) {
        require(numTokens <= balances[owner]);
        require(numTokens <= allowed[owner][msg.sender]);

        balances[owner] = balances[owner].sub(numTokens);
        allowed[owner][msg.sender] = allowed[owner][msg.sender].sub(numTokens);
        balances[buyer] = balances[buyer].add(numTokens);
        emit Transfer(owner, buyer, numTokens);
        return true;
    }
}

library SafeMath {
    function sub(uint256 a, uint256 b) internal pure returns (uint256) {
      assert(b <= a);
      return a - b;
    }

    function add(uint256 a, uint256 b) internal pure returns (uint256) {
      uint256 c = a + b;
      assert(c >= a);
      return c;
    }
}
ACassimiro commented 11 months ago

Just as an addendum. Subsequent runs of the test worked correctly, which is why I believe that what happened might be related to a non-handled network timeout or a related issue.

radumereuta commented 11 months ago

@ACassimiro I'm unable to reproduce the timing issue. Can you tell me a bit more about your environment? OS, locale settings. I've seen this kind of thing before when the local number format has a dot or a comma to separate decimals.

ACassimiro commented 11 months ago

I've tested it on a Mac M1 using Sonoma 14.1.2. VSCode is version 1.85. I've tried checking the locale in VSCode and it just says that it is "English (US)".

Regarding the network environment, I don't know how to reproduce it. I was having several issues with my internet service provider during the event, hence why I believe that it might be an unhandled timeout.