SRI-CSL / solidity

This is solc-verify, a modular verifier for Solidity.
https://github.com/SRI-CSL/solidity/blob/boogie/SOLC-VERIFY-README.md
GNU General Public License v3.0
50 stars 14 forks source link

Deep copy of arrays #99

Open dddejan opened 4 years ago

dddejan commented 4 years ago
pragma solidity >=0.5.0;

contract Test {
  struct S {
    int x;
  }
  S[] m_a;
  function test() external view {
    S[] memory a;
    a = m_a;
  }
}

Gives

solc-verify.py Test.sol --output .
Error while running verifier, details:
Parsing ./Test.sol.bpl
./Test.sol.bpl(42,85): Error: right-hand side in map store with wrong type: struct_storage_S#4_arr_type (expected: address_struct_memory_S#4_arr_type)
1 type checking errors detected in ./Test.sol.bpl

It's not clear how we support this. More meaningful error message would be good.

hajduakos commented 4 years ago

I agree. Will add a more meaningful error message until it gets supported

hajduakos commented 4 years ago

Meaningful error message in 60a0400