cerc-io/solidity
10
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
21,134 Commits 348 Branches 121 Tags 100 MiB
2fb8f1be5b
Commit Graph

667 Commits

Author SHA1 Message Date
Leo Alt
4c2b661eaa [SMTChecker] Report values for block, msg and tx variables in counterexamples 2021-10-05 15:19:10 +02:00
Leo Alt
d81ebe97c3 Fix magic access 2021-10-01 12:57:06 +02:00
chriseth
1531863835 Split Common.h into Numeric.h. 2021-09-23 15:27:29 +02:00
Leo Alt
e74f853c6b [SMTChecker] Support user types 2021-09-21 13:23:17 +02:00
Leo Alt
a1bea368cb [SMTChecker] Support constants via modules 2021-09-16 14:35:05 +02:00
Leo Alt
b731957e65 Fix BMCs constraints on internal functions 2021-09-15 14:42:39 +02:00
Leo Alt
6e2fe1e340 [SMTChecker] Cleanup spurious messages about TypeTypes 2021-09-07 16:55:25 +02:00
Leo Alt
106c591dde Support the external call option 2021-09-01 20:18:37 +02:00
Marenz
2b28f87abf Add type().min/max for enums 2021-09-01 15:02:02 +02:00
Leo Alt
ac528cfd1b add static array length constraint 2021-08-30 17:15:16 +02:00
Leo Alt
16bc15acac Fix false negative on storage array references returned by internal functions 2021-08-28 09:30:53 +02:00
Leo Alt
60b866f9d8 Fix ICE on multi-source use of abi.* 2021-08-27 18:55:36 +02:00
Leo Alt
8e81df1bd3 Do not show redundant unsupported errors in SMTChecker 2021-08-27 16:25:09 +02:00
Leonardo
6e6bbb2f83
Merge pull request #11837 from soroosh-sdi/use-range-v3-part2 
Using range-v3 instead of boost
 2021-08-26 09:38:27 +02:00
Leo Alt
61160aa0e7 Add constraints correlating address(this).balance and msg.value 2021-08-25 21:10:08 +02:00
Leo Alt
718f392849 Don't erase things for BMC if function call is staticcall 2021-08-25 14:09:46 +02:00
Leo Alt
a55685c04f Erase balances when delegatecall is seen 2021-08-25 12:39:26 +02:00
soroosh-sdi
b0ce98bcb2 Using range-v3 instead of boost 
Signed-off-by: soroosh-sdi <soroosh.sardari@gmail.com>
 2021-08-24 23:50:23 +04:30
Leo Alt
d89d63bf9c Use the nondeterministic interface also for BARECALL 2021-08-19 16:34:01 +02:00
chriseth
fe0d027d45
Merge pull request #11785 from ethereum/someMoreBaseFees 
Some more base fees.
 2021-08-12 19:48:10 +02:00
Leo Alt
6ee60aa628 Fix false positive on external calls from constructors 2021-08-12 18:51:55 +02:00
chriseth
90c4623460 Some more base fees. 2021-08-12 16:37:21 +02:00
Leo Alt
10397e440c Fix ICE in constants 2021-08-12 10:53:01 +02:00
Leo Alt
ee6285d6d7 Do not create VCs for underoverflow by default for Sol >=0.8 2021-08-09 14:12:31 +02:00
Leo Alt
08c065ee04 Add option divModWithSlacks 2021-08-06 15:50:25 +02:00
Leo Alt
685d7a8c99 Bundle all unproved targets in a single message and only show all if setting chooses that 2021-08-04 13:54:50 +02:00
Leo Alt
6c8ecfa82c Add option to choose solver 2021-07-27 17:14:21 +02:00
chriseth
e3525b81d0 Supply scanner to model checker. 2021-07-14 15:12:10 +02:00
chriseth
f75b55071e Remove CharStream from SourceLocation. 2021-07-14 15:12:07 +02:00
Kamil Śliwak
7d16c7b127 Equality operators for ModelCheckerSettings and ImportRemapper 2021-07-06 17:17:18 +02:00
chriseth
7d8a4e63d8
Merge pull request #11491 from TerranCivilian/fix-10269 
Remove unneeded include files
 2021-06-07 20:15:20 +02:00
TerranCivilian
c15501eea9 Remove unneeded include files 2021-06-07 12:53:18 -04:00
Leo Alt
bf21cd400c Fix conversion from bytes to fixed bytes 2021-06-01 17:55:18 +02:00
Leo Alt
547a6915ad Fix ICE on external calls from constructor 2021-06-01 14:21:48 +02:00
Leo Alt
f7b045b886 review 2021-05-26 22:12:49 +02:00
Leo Alt
95f973e08a Fix gasleft variable name 2021-05-26 22:12:49 +02:00
Leo Alt
daea5f886d Fix CHCSmtLib2Interface 2021-05-26 22:12:49 +02:00
Martin Blicha
9c98ab59f0 SMTChecker: fixed struct constructor where FixedBytes member is initialized with a string literal 2021-05-17 13:52:37 +02:00
Leonardo Alt
4b2ccf2f37 Abstract function smtchecker natspec 2021-05-11 15:30:19 +02:00
Leo Alt
e2959ce55c Assign cast from constants directly 2021-05-11 14:07:09 +02:00
Daniel Kirchner
6104ac1cdf Remove more imports of ranges namespace. 2021-05-07 15:42:17 +02:00
Leo Alt
1642c10f6e Fix ICE in free functions 2021-05-03 10:57:11 +02:00
Leonardo Alt
dd1865873e Choose contracts to be analyzed by the SMTChecker 2021-04-21 10:34:14 +02:00
Leonardo Alt
095d337140 Basic support to free constants 2021-04-19 19:23:18 +02:00
Leonardo Alt
4e34359063 Basic support to free functions 2021-04-19 19:23:18 +02:00
Leonardo Alt
e3abde43f5 Change settings.modelChecker.targets to take an array instead of string 2021-04-19 17:53:03 +02:00
Leonardo Alt
b753cb6120 Deprecate pragma experimental SMTChecker 2021-04-08 21:03:38 +02:00
chriseth
98a8640928
Merge pull request #11203 from anurag-git/issue_10738-1 
Use range-v3 loops (reverse, keys, values)
 2021-04-01 12:19:40 +02:00
anurag4u80
bbcdddeed9 Replaced keys, values and reverse with ranges 2021-03-31 23:33:04 +05:30
Martin Blicha
330fb8f4d0 [SMTChecker] Assignment refactoring 2021-03-31 13:36:50 +02:00