Comparing memory and storage values.

[michael-emmi]

It’s not clear how we can state postconditions for functions which update storage with memory-typed arguments, as in the following example:

$ cat a.sol && solc-verify.py a.sol 
pragma solidity ^0.5.0;

contract A {
    uint[] public ary;

    /// @notice postcondition __verifier_eq(ary, a)
    function f(uint[] memory a) public {
        ary = a;
    }
}
Error while running compiler, details:
Warning: This is a pre-release compiler version, please do not use it in production.

======= Converting to Boogie IVL =======

======= a.sol =======
Annotation:1:1: solc-verify error: Arguments must have the same type
__verifier_eq(ary, a)
^-------------------^
a.sol:7:5: solc-verify error: Error(s) while processing annotation for node
    function f(uint[] memory a) public {
    ^ (Relevant source part starts here and spans across multiple lines).

Perhaps it could be possible to allow comparisons between values whose Boogie-encoded types are comparable? Or maybe some form of casting?

[hajduakos]

This is tricky, because here the Boogie-encoded types are not comparable. A storage array is a datatype of an SMT array and a length, while a memory array is a reference to the former. Dereferencing would work in this case, but arrays/structures could be nested into each other so we would have to do that recursively. We might even automatically do this if the data location of the two arguments is different.