Commit Graph

4427 Commits

Author SHA1 Message Date
chriseth
6eea2f5c08
Merge pull request from a3d4/fix-ice-struct-with-mapping-assignment
Fix ICE caused by const structs with mappings
2021-01-13 15:19:02 +01:00
Leonardo
fe344ed6e5
Merge pull request from blishko/smt-refactoring
[SMTChecker] Refactoring common functionality
2021-01-13 14:23:19 +01:00
a3d4
35a25b107f Fix ICE caused by const structs with mappings 2021-01-12 18:39:54 +01:00
Martin Blicha
7c6340fe4f [SMTChecker] Refactoring expression to tuple assignment 2021-01-12 17:15:14 +01:00
Daniel Kirchner
162b1508da
Merge pull request from ethereum/useDropEx
Use drop_exactly.
2021-01-12 17:11:54 +01:00
chriseth
d97b9ba865
Merge pull request from ethereum/libraryCallGuard
Library call guard.
2021-01-12 16:52:24 +01:00
Leonardo
fa28e48415
Merge pull request from ethereum/smt_cex_internal_calls
[SMTChecker] Report internal calls in CHC transaction trace
2021-01-12 15:44:12 +01:00
chriseth
99add1e4e5
Merge pull request from ethereum/implicit-conversion-bug
Disallow certain implicit conversions between integer types.
2021-01-12 15:42:12 +01:00
Leonardo Alt
b3c3836388 Output internal calls 2021-01-12 14:57:04 +01:00
chriseth
24aded266e Dereference. 2021-01-12 14:28:27 +01:00
chriseth
7487a7d927 Use drop_exactly. 2021-01-12 14:01:10 +01:00
Leonardo Alt
f1ae24abc7 Remove extra line breaks 2021-01-12 14:00:07 +01:00
Leonardo
66a773aef9
Merge pull request from blishko/smt-try-catch
[SMTChecker] Support try-catch statements
2021-01-12 12:04:38 +01:00
hrkrshnn
e107d51f46 Disallow certain implicit conversions between integer types.
Disallow implicit conversion from ``uintN`` and ``intM`` when ``M > N``, and by extension, explicit
conversion between the same types are also disallowed.
2021-01-12 08:23:47 +01:00
chriseth
b9de0c6155 Use zip. 2021-01-11 20:54:28 +01:00
chriseth
5c453acbe8 Fix encoding of library return values. 2021-01-11 20:37:45 +01:00
chriseth
e807c9bb63 Library call guard. 2021-01-11 20:37:44 +01:00
chriseth
67d21a87c5
Merge pull request from ethereum/range-v3
Add range-v3.
2021-01-11 19:24:13 +01:00
Daniel Kirchner
eac2bcf72f Add range-v3. 2021-01-11 18:44:55 +01:00
Djordje Mijovic
85b8325f0b [Sol->Yul] Implementing dynamic array push for arrays of structs. 2021-01-11 17:49:42 +01:00
Djordje Mijovic
b06936b11c [refactor] Move copying struct to storage to it's own util function. 2021-01-11 16:26:14 +01:00
Martin Blicha
ff76c989ac addressing review comments 2021-01-11 14:19:06 +01:00
Martin Blicha
dd43ce1578 fixing try/catch encoding for BMC, refactoring 2021-01-11 13:36:03 +01:00
Martin Blicha
55589a9eec [SMTChecker] Basic support for try-catch in BMC 2021-01-11 13:36:02 +01:00
Martin Blicha
0f3924186e [SMTChecker] Support try-catch in CHC engine 2021-01-11 13:36:02 +01:00
chriseth
994fdb7517 Determine encoding type earlier. 2021-01-11 11:57:22 +01:00
Leonardo Alt
11f56861c3 Refactor cex loop 2021-01-07 23:13:02 +01:00
Harikrishnan Mulackal
5241b7b761
Merge pull request from ethereum/fixIRWrappingExp
Use wrapping arithmetic for exp in unchecked blocks.
2021-01-06 18:53:54 +01:00
Alex Beregszaszi
8edfa26f0a Mark the empty version pragma as invalid 2021-01-04 19:28:36 +00:00
Leonardo Alt
b02722ebda Add contract name to called function in cex 2021-01-04 10:03:16 +01:00
Djordje Mijovic
047d693ac9 Refactoring copyLiteralToMemoryFunction and reusing it from other functions.
Co-authored-by: Leonardo <leo@ethereum.org>

Co-authored-by: Alex Beregszaszi <alex@rtfs.hu>
2020-12-30 17:31:20 +01:00
Djordje Mijovic
ddb05769a5 [Sol->Yul] Implementing type name. 2020-12-30 17:19:03 +01:00
Leonardo Alt
78d55e6b4a [SMTChecker] Support check/unchecked 2020-12-30 12:14:30 +01:00
Martin Blicha
be0a0f4d90 [SMTChecker] Added constraints for block properties 2020-12-29 22:17:44 +01:00
Leonardo Alt
9482e7de23 [SMTChecker] Fix calls to virtual/overriden functions 2020-12-29 11:25:20 +01:00
Martin Blicha
bb0003f5ea removed extra parameter from PredicateInstance::nondetInterface 2020-12-28 19:48:48 +01:00
Martin Blicha
f76ff35225 [SMTChecker] Detect errors caused by reentrancy 2020-12-28 14:32:53 +01:00
Suriyaa Sundararuban
8649df169d
Update Natspec documentation URL 2020-12-27 14:55:40 +01:00
chriseth
2ab83217e3 Use wrapping arithmetic for exp in unchecked blocks. 2020-12-22 16:49:55 +01:00
chriseth
04d83af1d2
Merge pull request from ethereum/arrayClearingDiffBaseSol2Yul
[Sol->Yul] Fixing array clearing when copying from storage to storage.
2020-12-22 15:15:03 +01:00
Martin Blicha
d90b9da4f0 [SMTChecker] Refactoring 2020-12-22 13:10:48 +01:00
chriseth
0437ee7ad9 Fix length check when decoding error data. 2020-12-22 11:08:44 +01:00
chriseth
b965446182 Catch panic. 2020-12-22 11:08:44 +01:00
Đorđe Mijović
b78443ac75
Merge pull request from ethereum/deleteMappingSol2Yul
[Sol->Yul] Skipping mapping types when deleting structs and arrays.
2020-12-21 20:08:51 +01:00
Leonardo
a48106ca1f
Merge pull request from blishko/smt-virtual-modifiers-fix
[SMTChecker] Fix virtual modifier called statically
2020-12-21 18:05:02 +01:00
Djordje Mijovic
adb9d0c41a [Sol->Yul] Fixing array clearing when copying from storage to storage. 2020-12-21 17:33:06 +01:00
Djordje Mijovic
2d5a2c65a8 [Sol->Yul] Implementing getters for bytes and structs containing bytes member.
Co-authored-by: chriseth <chris@ethereum.org>
2020-12-21 14:46:06 +01:00
Martin Blicha
87ef0e16f5 [SMTChecker] Fix virtual modifier called statically 2020-12-21 13:52:28 +01:00
Djordje Mijovic
9b8634f2a7 [Sol->Yul] Skipping mapping types when deleting structs and arrays. 2020-12-21 13:19:25 +01:00
Leonardo
158154bac3
Merge pull request from ethereum/ir-runtime
Output runtime object in IR
2020-12-18 17:19:40 +01:00