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,635 Commits 348 Branches 121 Tags 100 MiB
29358806f4
Commit Graph

35 Commits

Author SHA1 Message Date
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
Leo Alt
9bcd2c18e4 Add expression substitution to Predicate 2021-10-26 11:30:30 +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
e74f853c6b [SMTChecker] Support user types 2021-09-21 13:23:17 +02:00
chriseth
90c4623460 Some more base fees. 2021-08-12 16:37: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
Leonardo Alt
4e34359063 Basic support to free functions 2021-04-19 19:23:18 +02:00
Leonardo Alt
ba97d6ac4e Add local vars to cex 2021-03-30 17:55:21 +02:00
Mathias Baumann
e197ebbdd1 Replace TypePointer with Type const* 2021-03-23 11:47:19 +01:00
Leonardo Alt
665ce27c18 Fix inheritance bug in CHC cex 2021-02-02 18:06:32 +01:00
Leonardo Alt
a612daa783 Add msgvalue to cex 2021-01-21 19:05:44 +01:00
Leonardo Alt
007d39871b [SMTChecker] Synthesize untrusted functions called externally 2021-01-15 11:56:26 +01:00
Leonardo Alt
b3c3836388 Output internal calls 2021-01-12 14:57:04 +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
2cbf33ca1c SMTChecker support ABI functions as UFs 2020-12-17 14:03:17 +01:00
Martin Blicha
eb356735f6 [SMTChecker] Adding support for reporting values of structs in CEX in CHC engine. 2020-12-08 16:40:28 +01:00
Leonardo Alt
7490ffbe13 Use nonlinear clauses instead of inlining for base constructors 2020-12-04 13:25:56 +01:00
Alex Beregszaszi
2f899bbffa [SMTChecker] Avoid implicit conversion 2020-11-11 16:29:03 +00:00
Leonardo Alt
25f75ce547 Remove nondet tests 2020-10-28 11:03:42 +00:00
Leonardo Alt
f2f84a7f97 Format array cex 2020-10-27 16:32:43 +00:00
Leonardo Alt
446e46fe06 Use Expression instead of plain strings for counterexamples 2020-10-27 12:04:51 +00:00
Leonardo Alt
54f76e081a [SMTChecker] Support crypto functions in CHC 2020-10-16 14:57:13 +01:00
Leonardo Alt
440e5b3935 [SMTChecker] Fix counterexample state reporting 2020-10-13 22:18:43 +01:00
Leonardo Alt
aec456021d Add tx constraints to CHC 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
3519b38055 Move predicate functions from CHC to PredicateInstance 2020-09-28 12:43:19 +02:00
Leonardo Alt
a3b6019131 Move post input and post output filtering from CHC to Predicate 2020-09-01 16:10:12 +02:00
Leonardo Alt
2e2e96cc93 Move state model filtering from CHC to Predicate 2020-09-01 16:10:12 +02:00
Leonardo Alt
e3a8c94ace Move formatFunctionCallCounterexample from CHC to Predicate 2020-09-01 16:10:11 +02:00
Leonardo Alt
016b9b83a8 Refactor predicates 2020-09-01 16:09:56 +02:00