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
15,422 Commits 348 Branches 121 Tags 100 MiB
7d3ccee921
Commit Graph

26 Commits

Author SHA1 Message Date
Leonardo Alt
ddc478e3e4 Add CallbackKind and use it for the SMT solver 2019-11-21 22:10:21 +00:00
Leonardo Alt
6b10efff8c Add CHCSmtLib2Interface 2019-11-07 11:12:11 +01:00
Leonardo Alt
ed9674be8d [SMTChecker] Add as const function to SMTLib2Interface 2019-09-18 22:57:14 +02:00
Leonardo Alt
a51577facf Fix Windows build 2019-09-02 22:37:30 +02:00
Leonardo Alt
a774b2d905 [SMTChecker] Zero-initialize arrays 2019-09-02 22:37:30 +02:00
Leonardo Alt
cce377833a Sort includes in libsolidity/formal 2018-12-17 18:26:10 +01:00
Leonardo Alt
f3c2309c73 Display better error message in SMTLib2 2018-11-23 09:43:49 +01:00
chriseth
bb10be789c Inject SMTLIB2 queries and responses via standard-json-io. 2018-11-23 09:43:49 +01:00
Leonardo Alt
20accf1a90 [SMTChecker] Add ArraySort and array operations 2018-11-22 14:04:20 +01:00
Leonardo Alt
13a142b039 [SMTChecker] Add FunctionSort and refactors the solver interface to create variables 2018-11-22 10:04:04 +01:00
Christian Parpart
87821c53c3 Isolating files shared between Yul- and Solidity language frontend. 2018-11-21 18:58:12 +00:00
Leonardo Alt
01ce43e51b [SMTChecker] Refactor smt::Sort and its usage 2018-11-21 15:46:47 +01:00
Leonardo Alt
70bb0eaf95 [SMTChecker] Implement uninterpreted functions and use it for blockhash() 2018-11-15 09:12:42 +01:00
Leonardo Alt
f249f9c86f [SMTLib2] Fix repeated declarations 2018-07-27 17:34:44 +01:00
Alex Beregszaszi
dea0567e06 Fix unterminated parentheses typo in SMTLib2 
Found by @leonardoalt
 2018-07-27 17:33:53 +01:00
Leonardo Alt
87a38e1abe [SMTChecker] SMTPortfolio: use all SMT solvers available 2018-07-27 16:15:34 +01:00
Leonardo Alt
06dbcb3afe Only ask for a model if it's SAT 2018-07-27 14:13:22 +02:00
chriseth
762d591a47 Introduce sorts for smt expressions. 2017-11-22 15:20:26 +01:00
Alex Beregszaszi
18ae0c3d78 SMT enforce variable types 2017-10-05 12:29:20 +01:00
chriseth
cf5e1d6120 Review changes. 2017-08-23 17:37:35 +02:00
chriseth
1e05ebe50e Refactor Z3 read callback. 2017-08-23 17:37:35 +02:00
chriseth
9ac2ac14c1 Rename read file callback. 2017-08-23 17:37:35 +02:00
chriseth
4cea3d4aa4 Insert abstraction layer. 2017-08-23 17:37:35 +02:00
chriseth
b3f8ed457a Cleanup. 2017-08-23 14:24:30 +02:00
chriseth
39fc798999 Use file to communicate with z3. 2017-08-23 14:24:05 +02:00
chriseth
df848859da Rewrite using SMTLIB2 interface. 2017-08-23 14:24:05 +02:00