strings not passed/returned/cast properly to/from functions/modifiers

[dddejan]

pragma solidity >=0.5.0;
contract A {
    modifier m(string memory msg) { _; }
    function f() public m("heyheyhey") {}
}

gives

$ solc-verify.py modifier_string.sol --output .
Error while running verifier, details:
Parsing ./modifier_string.sol.bpl
./modifier_string.sol.bpl(23,1): Error: mismatched types in assignment command (cannot assign int_arr_type to int_arr_ptr)
1 type checking errors detected in ./modifier_string.sol.bpl

[dddejan]

Another example

pragma solidity >=0.5.0;
contract A {
  uint x;
  function f(bytes32 b) public view returns (uint) {
      return x;
  }
  function g() public view returns (uint) {
    return f("heyheyhey");
  }
}

Currently gives

$ solc-verify.py issue.sol --output .
Error while running verifier, details:
Parsing ./issue.sol.bpl
./issue.sol.bpl(38,1): Error: mismatched types in assignment command (cannot assign int_arr_type to int)
1 type checking errors detected in ./issue.sol.bpl

[dddejan]

Another example

pragma solidity >=0.5.0;
contract A {
  bytes32 public constant name = "heyheyhey";
  function f() view public returns(bytes32) {
    return name;
  }
}

Currently gives

$ solc-verify.py issue.sol --output .
Error while running verifier, details:
Parsing ./issue.sol.bpl
./issue.sol.bpl(21,1): Error: mismatched types in assignment command (cannot assign int_arr_type to int)
1 type checking errors detected in ./issue.sol.bpl

[dddejan]

Another example

pragma solidity >=0.5.0;
contract A {
  bytes32 name = "heyheyhey";
}

Gives

$ solc-verify.py issue.sol --output .
Error while running verifier, details:
Parsing ./issue.sol.bpl
./issue.sol.bpl(23,28): Error: right-hand side in map store with wrong type: int_arr_type (expected: int)
1 type checking errors detected in ./issue.sol.bpl