cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #6647 from ethereum/smt_tuple_decl

Browse Source 
[SMTChecker] Support tuple type declaration
This commit is contained in:
chriseth
2019-05-02 12:49:50 +02:00
committed by GitHub
parent d4c4a473d8 6c7527ac90
commit 54775a7880
13 changed files with 97 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files
test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol
-1
View File
@@ -12,4 +12,3 @@ contract C
}
// ----
// Warning: (153-156): Assertion checker does not yet implement tuples and inline arrays.
test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol
-1
View File
@@ -12,5 +12,4 @@ contract C
}
// ----
// Warning: (153-156): Assertion checker does not yet implement tuples and inline arrays.
// Warning: (163-176): Assertion violation happens here
test/libsolidity/smtCheckerTests/types/address_transfer.sol
-1
View File
@@ -12,5 +12,4 @@ contract C
}
// ----
// Warning: (131-146): Insufficient funds happens here
// Warning: (131-146): Assertion checker does not yet implement this type.
// Warning: (195-219): Assertion violation happens here
test/libsolidity/smtCheckerTests/types/address_transfer_2.sol
-2
View File
@@ -15,7 +15,5 @@ contract C
}
// ----
// Warning: (217-232): Insufficient funds happens here
// Warning: (217-232): Assertion checker does not yet implement this type.
// Warning: (236-251): Insufficient funds happens here
// Warning: (236-251): Assertion checker does not yet implement this type.
// Warning: (295-324): Assertion violation happens here
test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol
-2
View File
@@ -12,7 +12,5 @@ contract C
}
// ----
// Warning: (134-149): Insufficient funds happens here
// Warning: (134-149): Assertion checker does not yet implement this type.
// Warning: (153-169): Insufficient funds happens here
// Warning: (153-169): Assertion checker does not yet implement this type.
// Warning: (213-237): Assertion violation happens here
test/libsolidity/smtCheckerTests/types/array_literal_1.sol
+1 -1
View File
@@ -8,5 +8,5 @@ contract C
}
// ----
// Warning: (76-96): Unused local variable.
// Warning: (99-114): Assertion checker does not yet implement tuples and inline arrays.
// Warning: (99-114): Assertion checker does not yet implement inline arrays.
// Warning: (99-114): Internal error: Expression undefined for SMT solver.
test/libsolidity/smtCheckerTests/types/tuple_assignment_compound.sol
+13
View File
@@ -0,0 +1,13 @@
pragma experimental SMTChecker;
contract C
{
function f() public pure {
uint a = 1;
uint b = 3;
a += ((((b))));
assert(a == 3);
}
}
// ----
// Warning: (122-136): Assertion violation happens here