diff options
| author | chriseth <chris@ethereum.org> | 2018-10-25 19:01:01 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-25 19:01:01 +0800 |
| commit | c36a3bd683372934016517bb5ee0e7a4539d42a7 (patch) | |
| tree | 6712724552fd72d2e05c0c6f7e86e124e779d6ae /test | |
| parent | f714b0dd7c0b48ea2b93855e1cda9d1101b3f35c (diff) | |
| parent | d8cbf321dafbe85f6fde07b5dd4ce7a3abffaeb6 (diff) | |
| download | dexon-solidity-c36a3bd683372934016517bb5ee0e7a4539d42a7.tar.gz dexon-solidity-c36a3bd683372934016517bb5ee0e7a4539d42a7.tar.zst dexon-solidity-c36a3bd683372934016517bb5ee0e7a4539d42a7.zip | |
Merge pull request #5283 from ethereum/smt_fixed_bytes
[SMTChecker] Support FixedBytes
Diffstat (limited to 'test')
| -rw-r--r-- | test/libsolidity/smtCheckerTests/special/blockhash.sol | 4 | ||||
| -rw-r--r-- | test/libsolidity/smtCheckerTests/special/msg_sig.sol | 4 | ||||
| -rw-r--r-- | test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol | 16 |
3 files changed, 16 insertions, 8 deletions
diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol index d0f263eb..1c693914 100644 --- a/test/libsolidity/smtCheckerTests/special/blockhash.sol +++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol @@ -7,8 +7,4 @@ contract C } } // ---- -// Warning: (86-98): Assertion checker does not yet support this special variable. -// Warning: (86-98): Assertion checker does not yet implement this type. -// Warning: (86-102): Assertion checker does not yet implement the type bytes32 for comparisons -// Warning: (86-102): Internal error: Expression undefined for SMT solver. // Warning: (79-103): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/msg_sig.sol b/test/libsolidity/smtCheckerTests/special/msg_sig.sol index 6f832179..109470a8 100644 --- a/test/libsolidity/smtCheckerTests/special/msg_sig.sol +++ b/test/libsolidity/smtCheckerTests/special/msg_sig.sol @@ -7,8 +7,4 @@ contract C } } // ---- -// Warning: (86-93): Assertion checker does not yet support this special variable. -// Warning: (86-93): Assertion checker does not yet implement this type. -// Warning: (86-107): Assertion checker does not yet implement the type bytes4 for comparisons -// Warning: (86-107): Internal error: Expression undefined for SMT solver. // Warning: (79-108): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol b/test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol new file mode 100644 index 00000000..541fff54 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/fixed_bytes_1.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C +{ + bytes32 x; + function f(bytes8 y) public view { + assert(x != y); + assert(x != g()); + } + function g() public view returns (bytes32) { + return x; + } +} +// ---- +// Warning: (96-110): Assertion violation happens here +// Warning: (114-130): Assertion violation happens here |