cerc-io/solidity
16
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
23,595 Commits 348 Branches 121 Tags 100 MiB
712229a5c6
Commit Graph

709 Commits

Author SHA1 Message Date
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
Leonardo
78d94737a4
Merge pull request #11188 from blishko/issue-11181 
[SMTChecker] Fix crash when analysing try-catch clauses with function call.
 2021-03-31 11:24:36 +02:00
chriseth
b04b189959 Syntax for custom errors. 2021-03-30 21:15:18 +02:00
Martin Blicha
2d231f1859 [SMTChecker] Changed SMTEncoder::mergeVariables to work regardless which branch has been visited first 2021-03-30 20:35:44 +02:00
Leonardo Alt
ba97d6ac4e Add local vars to cex 2021-03-30 17:55:21 +02:00
Leonardo Alt
dbd067d6db Report out of bounds index access 2021-03-30 10:28:48 +02:00
Leonardo Alt
d1db41a5c8 Fix target warning order nondeterminism 2021-03-26 12:13:52 +01:00
Martin Blicha
85358dfe30 [SMTChecker] Do not create targets for contracts that cannot be deployed 2021-03-25 15:38:37 +01:00
Martin Blicha
5293f05ee3 [SMTChecker] Fix ICE on ABI functions with no arguments 2021-03-25 13:28:29 +01:00
Martin Blicha
98446782e2 [SMTChecker] Fix compound assignment to push 2021-03-24 14:54:13 +01:00
Martin Blicha
852e877ae7 [SMTChecker] Handle InaccessibleDynamicType 2021-03-24 11:53:06 +01:00
Mathias Baumann
e197ebbdd1 Replace TypePointer with Type const* 2021-03-23 11:47:19 +01:00
Leonardo
25b31111df
Merge pull request #11040 from ethereum/smt_fix_virtual_one_more_time 
[SMTChecker] Fix bug in virtual functions called by constructor
 2021-03-17 16:54:36 +01:00
Martin Blicha
432944d0b4 [SMTChecker] Small refactoring of defining SMT expressions for structs/tuples 2021-03-16 15:34:43 +01:00
Martin Blicha
2f52affcc2 [SMTChecker] Correctly resolve current scope contract in VariableUsage. 2021-03-15 13:55:14 +01:00
Martin Blicha
6aa6c5f5f9 [SMTChecker] Reset reference variables on assignment to a variable of reference type 2021-03-12 19:51:31 +01:00
Leonardo Alt
998346e599 Fix bug in virtual functions called by constructor. 2021-03-12 16:42:28 +01:00
Martin Blicha
0cb75293f9 [SMTChecker] fix handling of assignments of array/mapping state variable accessed using contract name 2021-03-12 14:01:07 +01:00
Leonardo Alt
6fd76e830d Fix CHC cex order 2021-03-11 10:36:40 +01:00
Martin Blicha
4285c2803b [SMTChecker] Fix ICE on array.pop nested inside 1-tuple 2021-03-09 20:00:51 +01:00
Martin Blicha
5af01f6896 [SMTChecker] Use same sort name for array slice as for the underlying array. 2021-03-09 11:06:22 +01:00
Martin Blicha
385a664f3c [SMTChecker] Fix public getter for array of structs. 2021-03-08 17:34:20 +01:00
Martin Blicha
0340510c53 [SMTChecker] correct handling of FixedBytes constants initialized with string literal 2021-03-04 15:14:47 +01:00
Martin Blicha
41fc59f00f [SMTChecker] Ensure that push to a string casted to bytes is registered in the original string 2021-03-03 17:11:42 +01:00
Martin Blicha
41a01de664 [SMTChecker] fix crash on push to string casted to bytes 2021-03-03 15:25:32 +01:00
Alexander Arlt
ae6996efc1 Fix issue with pop on storage array. 2021-02-23 14:26:55 +01:00
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
d99256aae7 [SMTChecker] refactoring of resetting storage variables 2021-02-03 15:53:58 +01:00
Martin Blicha
f1013427a7 [SMTChecker] refactoring the accessing the encoding state 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
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
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
504e4c22b2 [SMTChecker] Fix in abi handling - tuple expression of size 1 has the type of the member and not TupleType 2021-01-14 14:53:56 +01:00
Martin Blicha
b4d2a71eec [SMTChecker] Fix in abi handling - fixed missing type conversion 2021-01-14 14:53:44 +01:00
Martin Blicha
32a923c7ef [SMTChecker] Fix in abi handling - abstracting expressions of type Function inside ABI functions when translating to SMT 2021-01-14 14:53:22 +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
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
Leonardo Alt
11f56861c3 Refactor cex loop 2021-01-07 23:13:02 +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
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
Martin Blicha
d90b9da4f0 [SMTChecker] Refactoring 2020-12-22 13:10:48 +01:00