Support for delete of memory types

[dddejan]

pragma solidity ^0.5.0;
contract Test {
    function test(uint n) public pure {
        require(n > 0);
        int[] memory a = new int[](1);
        delete a;
        assert(a.length == 0);
    }
}

Delete is currently unsupported. As it is basically initialization, it might not be too hard to support.

Currently:

solc-verify.py Test.sol --verbose --output .
Solc command: /Users/dejan/workspace/solidity-sri/build/solc/solc  --boogie Test.sol -o . --overwrite --boogie-arith int
----- Compiler output -----
Warning: This is a pre-release compiler version, please do not use it in production.

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

======= Test.sol =======
Test.sol:7:9: solc-verify error: Delete is only supported for value types and storage (non-pointer)
        delete a;
        ^------^
Test.sol:4:5: solc-verify warning: Errors while translating function body, will be skipped
    function test(uint n) public pure {
    ^ (Relevant source part starts here and spans across multiple lines).

---------------------------
Using cvc4 at /usr/local/bin/cvc4
Verifier command: mono /Users/dejan/workspace/boogie/Binaries/Boogie.exe ./Test.sol.bpl /nologo /doModSetAnalysis /errorTrace:0 /useArrayTheory /trace /cvc4exe:/usr/local/bin/cvc4 /proverOpt:SOLVER=CVC4
----- Verifier output -----
Parsing ./Test.sol.bpl
Coalescing blocks...
Inlining...

Running abstract interpretation...
  [0.027088 s]
[TRACE] Using prover: /usr/local/bin/cvc4

Verifying __constructor#34 ...
  [0.171 s, 0 proof obligations]  verified

Boogie program verifier finished with 1 verified, 0 errors

---------------------------
DeleteMemoryArrayDynamic::[implicit_constructor]: OK
DeleteMemoryArrayDynamic::test: SKIPPED
Use --show-warnings to see 1 warning.
Some functions were skipped. Use --verbose to see details.
No errors found.