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,856 Commits 348 Branches 121 Tags 100 MiB
develop
Commit Graph

715 Commits

Author SHA1 Message Date
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
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