cerc-io/solidity
15
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
19,585 Commits 348 Branches 121 Tags 100 MiB
fc7a091bfb
Commit Graph

385 Commits

Author SHA1 Message Date
Leonardo
7405dc5b7f
Merge pull request #10836 from ethereum/smt_fix_cex_inheritance 
Fix inheritance bug in CHC cex
 2021-02-03 18:49:25 +01:00
Martin Blicha
4bcdac71df [SMTChecker] updates to the tests 2021-02-03 15:53:58 +01:00
Leonardo Alt
665ce27c18 Fix inheritance bug in CHC cex 2021-02-02 18:06:32 +01:00
Martin Blicha
a49950cdf3 [SMTChecker] Added transaction constraints also for contract deployment 2021-02-01 16:46:34 +01:00
Leonardo Alt
545305a31f [SMTChecker] Fix super and virtual 2021-01-28 18:51:29 +01:00
Martin Blicha
deb90d84a6 [SMTChecker] added missing type constraints for Address 2021-01-27 20:39:24 +01:00
Martin Blicha
484e67815a [SMTChecker] Basic support for inline assembly using over-approximating analysis 2021-01-26 16:20:50 +01:00
Leonardo Alt
40221a90c4 Update smtCheckerTests for z3 4.8.10 2021-01-26 10:18:52 +01:00
Leonardo Alt
a612daa783 Add msgvalue to cex 2021-01-21 19:05:44 +01:00
Leonardo Alt
3b23cadbdc Add CLI and JSON option to select SMTChecker targets 2021-01-20 17:35:37 +01:00
Martin Blicha
35d228d9b6 [SMTChecker] Gather local variables also from nested try/catch clauses 2021-01-18 18:30:18 +01:00
Leonardo Alt
c7ca87c012 Fix static virtual resolution 2021-01-18 16:23:38 +01:00
Alex Beregszaszi
e117c9516e Replace "pragma experimental ABIEncoderV2" in tests where appropriate 
And add a few tests for "pragma abicoder".
 2021-01-15 19:57:09 +00:00
Martin Blicha
18214d1ccc [SMTChecker] Reset checked/unchecked flag to the default value when inlining function in BMC 2021-01-15 15:36:26 +01:00
Leonardo Alt
007d39871b [SMTChecker] Synthesize untrusted functions called externally 2021-01-15 11:56:26 +01:00
Martin Blicha
2ee0f347b9 [SMTChecker] additional regression tests 2021-01-14 14:54:14 +01:00
Martin Blicha
5e13744423 [SMTChecker] Fixed pushing string literal to bytes array 2021-01-13 16:30:50 +01:00
Martin Blicha
7c6340fe4f [SMTChecker] Refactoring expression to tuple assignment 2021-01-12 17:15:14 +01:00
Leonardo Alt
b3c3836388 Output internal calls 2021-01-12 14:57:04 +01:00
Leonardo Alt
f1ae24abc7 Remove extra line breaks 2021-01-12 14:00:07 +01:00
Martin Blicha
ff76c989ac addressing review comments 2021-01-11 14:19:06 +01:00
Martin Blicha
3d7188ac7b update to the tests 2021-01-11 13:36:03 +01:00
Martin Blicha
09de54b5eb tests 2021-01-11 13:36:03 +01:00
Leonardo Alt
b02722ebda Add contract name to called function in cex 2021-01-04 10:03:16 +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
41d31fe4d4 updates to the tests 2020-12-28 20:05:52 +01:00
Martin Blicha
77dff222e9 disabling some tests because of nondeterminism in Spacer 2020-12-28 16:24:44 +01:00
Martin Blicha
745466b71f updates to the tests 2020-12-28 14:32:53 +01:00
Martin Blicha
d90b9da4f0 [SMTChecker] Refactoring 2020-12-22 13:10:48 +01:00
Martin Blicha
87ef0e16f5 [SMTChecker] Fix virtual modifier called statically 2020-12-21 13:52:28 +01:00
Leonardo Alt
034d1ab90f [SMTChecker] Replace constants by their value in-place 2020-12-18 14:22:28 +01:00
Martin Blicha
7078e8f8f8 [SMTChecker] Fix analysis of overriding modifiers 2020-12-17 17:05:54 +01:00
Leonardo Alt
50be39fc21 Add and update tests 2020-12-17 14:42:49 +01:00
Leonardo Alt
f5c96ea6da Fix constant evaluation build 2020-12-16 17:59:00 +01:00
chriseth
3a23df6717 Merge remote-tracking branch 'origin/develop' into breaking 2020-12-16 16:56:45 +01:00
Leonardo Alt
80e85b772b [SMTChecker] Apply const eval to arithmetic binary expressions 2020-12-16 14:58:00 +01:00
Leonardo Alt
59428b8f76 Fix SMTChecker tests on breaking 2020-12-15 19:49:57 +01:00
chriseth
ffaf40950a
Merge pull request #10605 from ethereum/develop 
Merge develop into breaking.
 2020-12-15 14:01:01 +01:00
Martin Blicha
e2c27b8ea4 [SMTChecker] Fix internal error on constructor of a recursive struct 2020-12-15 09:53:52 +01:00
Martin Blicha
71f835b71b [SMTChecker] Fixed internal error when increment/decrement is applied on a result of push(). 2020-12-14 22:52:44 +01:00
Alex Beregszaszi
edbdff8619 Update tests 2020-12-14 19:32:31 +00:00
Martin Blicha
103fa3b7eb [SMTChecker] Fix internal error on abstract modifier 2020-12-14 18:23:25 +01:00
Martin Blicha
27402781c4 [SMTChecker] Fixed crash on push to bytes on lhs of an assignment 2020-12-14 17:40:45 +01:00
Martin Blicha
0be325dc0d [SMTChecker] Fix handling of function calls where the function identifier is nested in a tuple. 2020-12-14 16:19:24 +01:00
chriseth
0dd2f1edbe Update counter-examples. 2020-12-14 14:21:35 +01:00
chriseth
561280a5cc Merge remote-tracking branch 'origin/develop' into breaking 2020-12-14 11:33:40 +01:00
Martin Blicha
8927015e5a [SMTChecker] Adding unary increment and decrement as under/overflow verification targets for the CHC engine 2020-12-11 17:41:50 +01:00
Leonardo Alt
64f81fe82b Fix SMT tests 2020-12-10 18:54:52 +01:00