Verisol crashes on contracts with array allocation

[fredfeng]

Execute Verisol with a simple contract that contains a new statement:

dotnet Binaries/VeriSol.dll C1-buggy.sol C1 /omitSourceLineInfo /omitDataValuesInTrace /omitAxioms /omitHarness /omitUnsignedSemantics

Expected: Generate the right .BPL file.

Got:

Command line args ==> /Users/yufeng/research/LoopSum/examples/C1-buggy.sol, C1, /omitSourceLineInfo, /omitDataValuesInTrace, /omitAxioms, /omitHarness, /omitUnsignedSemantics
SpecFilesDir = /Users/yufeng/research/LoopSum/examples

++ Running Solc on /Users/yufeng/research/LoopSum/examples/C1-buggy.sol....
C1-buggy.sol:14:21: TypeError: Type address is not implicitly convertible to expected type uint256.
	      tempLockTime[_address][i] = lockTime[_address][i] + later-earlier;
	                   ^------^

C1-buggy.sol:14:8: TypeError: Indexed expression has to be a type, mapping or array (is uint256)
	      tempLockTime[_address][i] = lockTime[_address][i] + later-earlier;
	      ^--------------------^

Here is C1-buggy.sol:

pragma solidity ^0.5.10;

contract C1 {

    mapping (address => uint256[]) private lockTime;
    mapping (address => uint256) private lockNum;
    uint later = 1;
    uint earlier = 2;

    function foo(address _address) public {

        uint256[] memory tempLockTime = new uint256[](lockNum[_address]);
	for (uint i = 0; i < lockNum[_address]; ++i) {
	      tempLockTime[_address][i] = lockTime[_address][i] + later-earlier;
	}

    }
}

[shuvendu-lahiri]

Thanks. There is indeed a problem with new T allocations, when T is of type array.

However, the error showsn above are errors from Solidity compiler. Can you fix the example so we see the VeriSol translation error?

[shuvendu-lahiri]

Test/regressions/ArrayAlloc.sol