Commit Graph
4619 Commits
Author SHA1 Message Date
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 #10721 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 #10737 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 #10684 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
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 #10492 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 #10577 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 #10670 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 Mijovicandchriseth 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 #10345 from ethereum/ir-runtime
Output runtime object in IR
2020-12-18 17:19:40 +01:00
Alex Beregszaszi 7e20a095a8 Merge pull request #10652 from ethereum/smt_constants_inplce
[SMTChecker] Replace constants by their value in-place
2020-12-18 14:22:32 +00:00
chriseth c4ade1753e Merge pull request #10445 from ethereum/modifiers
[Sol->Yul] Implement function modifiers.
2020-12-18 14:29:00 +01:00
Leonardo Alt 034d1ab90f [SMTChecker] Replace constants by their value in-place 2020-12-18 14:22:28 +01:00
Alex Beregszaszi b14a6a10cc Report meaningful error if parsing a version pragma failed 2020-12-18 11:50:37 +00:00
Martin Blicha 7078e8f8f8 [SMTChecker] Fix analysis of overriding modifiers 2020-12-17 17:05:54 +01:00
chriseth 35908c602b Modifiers for constructors. 2020-12-17 17:00:51 +01:00
chriseth ccaa81fbe7 Implement function modifiers. 2020-12-17 17:00:51 +01:00
Leonardo Alt 2cbf33ca1c SMTChecker support ABI functions as UFs 2020-12-17 14:03:17 +01:00