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
22,054 Commits 348 Branches 121 Tags 100 MiB
43f29c00da
Commit Graph

687 Commits

Author SHA1 Message Date
Daniel Kirchner
0f1a63c3fa Fix import directive visits in type checker and view pure checker. 2022-03-14 14:53:06 +01:00
Tyler
047034544e Merge branch 'develop' of github.com:tfire/solidity into fix/remove-namespace-ast-annotations 2022-03-09 18:55:22 -05:00
Tyler
519e1c9402 Specify namespaces 
Fix references into solidity::util
 2022-03-08 00:09:17 -05:00
wechman
52dfccca98 Replace all locale-dependent operations with locale-agnostic counterparts 2022-03-07 17:23:08 +01:00
nishant-sachdeva
cc6344c03c Changed instaces of isByteArrayOrString() to isByteArray() where it's only supposed to return a True for Bytes Type 2022-02-02 17:05:26 +05:30
nishant-sachdeva
9043621747 Changed occurences of isByteArray() to isByteArrayOrString(). The idea 
is to, in a future commit, replace such occurences of
isByteArrayOrString() which are required to return True only for Bytes
type with a new isByteArray() function.
 2022-02-02 14:19:58 +05:30
Leo Alt
fb8c138b8b Do not analyze unecessary contracts 2021-12-24 19:36:32 +01:00
Marenz
7a96953e78 Implement typechecked abi.encodeCall() 2021-12-16 17:35:58 +01:00
Leo Alt
316be7206f Fix soundness of storage/memory pointers that were not erasing enough knowledge 2021-12-14 12:02:18 +01:00
Leo Alt
16535aae32 Fix ICE when unsafe targets are solved more than once and the cex is different 2021-12-03 00:21:38 +01:00
Leo Alt
dff280cadc Fix ICE in CHC when using gas in the function options 2021-11-03 15:40:54 +01:00
Leo Alt
e40cf92b1d [SMTChecker] Merge all entry points for a target 2021-11-03 11:12:58 +01:00
Leo Alt
37215ffcfd Add SMTCheckerTest isoltest option to ignore invariants 2021-10-26 11:30:30 +02:00
Leo Alt
d419c30ca6 Add errorCode list to invariants report 2021-10-26 11:30:30 +02:00
Leo Alt
49e7627bd3 Use invariants in CHC 2021-10-26 11:30:30 +02:00
Leo Alt
bc90533c93 Add invariants to ModelCheckerSettings 2021-10-26 11:30:30 +02:00
Leo Alt
d554824f70 Add Invariants which traverses the proof and collects invariants for the given predicates 2021-10-26 11:30:30 +02:00
Leo Alt
9bcd2c18e4 Add expression substitution to Predicate 2021-10-26 11:30:30 +02:00
Leo Alt
ce72d7cd26 Add ExpressionFormatter which translates an smtutil::Expression into a Solidity-like expression string 2021-10-26 11:30:30 +02:00
tcoyvwac
ba0c09e082
Prefer make_unique over new 2021-10-15 19:46:47 +02:00
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