solidity

solidity copied to clipboard

Equality of memory arrays from storage copies.

8

I expected the following to work: ``` $ cat a.sol && solc-verify.py a.sol ``` ```solidity pragma solidity ^0.5.0; /// @notice invariant __verifier_eq(a1, a2) contract C { int[] a1; int[] a2;...

michael-emmi

Overridden virtual functions: internal compile error.

4

It seems that overriding an inherited virtual function causes a crash! Not clear whether this is something you want to deal with, since (a) this example also crashes `solc`, and...

michael-emmi

Comparing memory and storage values.

1

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...

michael-emmi

- test/libsolidity/syntaxTests/modifiers/function_modifier_invocation_parameters.sol - test/libsolidity/syntaxTests/modifiers/function_modifier_invocation.sol ```solidity contract B { function f(uint8 a) mod1(a, true) mod2(r) pure public returns (bytes7 r) { } modifier mod1(uint a, bool b) { if (b) _;...

dddejan

Although we don't support functions, an appropriate message should be reported ```solidity contract C { function f() public returns (bool ret) { return f == f; } function g() public...

dddejan

When I tried to run the example of Readme at [Docker](https://github.com/SRI-CSL/solidity/tree/0.7/docker) directory, I got an error: I also commented on the second line of `Annotations.sol`, so there is not this...

guialvares