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

27 Commits

Author SHA1 Message Date
Nikola Matic
d0a5556fd0 Purge using namespace from libsolidity/formal 2023-08-15 14:40:27 +02:00
Leo Alt
8d91ccf028 [SMTChecker] Add a new trusted mode which assumes that code that is 
available at compile time is trusted.
 2023-02-06 17:02:33 +01:00
Rodrigo Q. Saramago
feba4de509
Add paris constraints to SMTChecker 
Co-authored-by: Daniel <daniel@ekpyron.org>
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
Co-authored-by: Leo <leo@ethereum.org>
 2023-01-31 11:03:04 +01:00
Marenz
f7cc29bec1 Add std:: qualifier to move() calls 2022-08-30 11:12:15 +02:00
Tyler
519e1c9402 Specify namespaces 
Fix references into solidity::util
 2022-03-08 00:09:17 -05:00
Marenz
7a96953e78 Implement typechecked abi.encodeCall() 2021-12-16 17:35:58 +01:00
Leo Alt
e74f853c6b [SMTChecker] Support user types 2021-09-21 13:23:17 +02:00
Leo Alt
60b866f9d8 Fix ICE on multi-source use of abi.* 2021-08-27 18:55:36 +02:00
Leo Alt
61160aa0e7 Add constraints correlating address(this).balance and msg.value 2021-08-25 21:10:08 +02:00
chriseth
90c4623460 Some more base fees. 2021-08-12 16:37:21 +02:00
Mathias Baumann
e197ebbdd1 Replace TypePointer with Type const* 2021-03-23 11:47:19 +01:00
Martin Blicha
a49950cdf3 [SMTChecker] Added transaction constraints also for contract deployment 2021-02-01 16:46:34 +01:00
Leonardo Alt
a612daa783 Add msgvalue to cex 2021-01-21 19:05:44 +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
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
be0a0f4d90 [SMTChecker] Added constraints for block properties 2020-12-29 22:17:44 +01:00
Leonardo Alt
2cbf33ca1c SMTChecker support ABI functions as UFs 2020-12-17 14:03:17 +01:00
Alex Beregszaszi
2f899bbffa [SMTChecker] Avoid implicit conversion 2020-11-11 16:29:03 +00:00
Leonardo Alt
54f76e081a [SMTChecker] Support crypto functions in CHC 2020-10-16 14:57:13 +01:00
Leonardo Alt
a2cdde1191 Add tx data to symbolic state 2020-10-13 17:49:04 +01:00
Leonardo Alt
18cf01c187 Add this and state to CHC 2020-10-12 11:11:52 +01:00
Leonardo Alt
a86f656704 Refactor state as tuple 2020-10-12 11:11:52 +01:00
Leonardo Alt
ac93ee1d08 Move error flag from CHC to SymbolicState 2020-09-28 12:37:57 +02:00
Sachin Grover
b7adb2aa42 Add SPDX license identifier if not present already in source file 
Fixes: #9220
 2020-07-17 20:24:12 +05:30
Leonardo Alt
45eba27424 Rename namespace 2020-05-20 12:55:18 +02:00
Leonardo Alt
a0c605aa85 [SMTChecker] Support array length 2020-05-14 23:32:29 +02:00
Leonardo Alt
05a85461fe Symbolic state 2020-04-06 12:27:53 +02:00