 Leonardo Alt
|
d87e15e2cd
|
Refactor CHC sorts
|
2020-09-15 16:45:50 +02:00 |
|
|
Leonardo Alt
|
23ee011c56
|
[SMTChecker] Fix imports
|
2020-09-11 13:34:46 +02:00 |
|
|
Leonardo Alt
|
00f6b303b1
|
[SMTChecker] Change warning message
|
2020-09-09 16:14:21 +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
|
5bbb20d3cb
|
Move stateVariablesIncludingInheritedAndPrivate from CHC to SMTEncoder
|
2020-09-01 16:09:57 +02:00 |
|
|
Leonardo Alt
|
016b9b83a8
|
Refactor predicates
|
2020-09-01 16:09:56 +02:00 |
|
 chriseth
|
4dc63875f9
|
Merge pull request #9113 from ethereum/smt_chc_overflow
[SMTChecker] Add underflow/overflow target to CHC
|
2020-08-20 13:17:00 +02:00 |
|
|
Leonardo Alt
|
8a06041bbe
|
[SMTChecker] Add underflow/overflow target to CHC
|
2020-08-14 12:58:27 +02:00 |
|
 Jason Cobb
|
888d7037cd
|
Make FunctionCallAnnotation::kind a SetOnce
|
2020-08-12 11:57:01 -04:00 |
|
|
Leonardo Alt
|
8df8c6e14f
|
[SMTChecker] Fix ICE in BMC function inlining
|
2020-08-05 11:47:25 +02:00 |
|
|
Leonardo Alt
|
d5f00842d9
|
cex2dot debug
|
2020-07-23 18:49:03 +02:00 |
|
|
Leonardo Alt
|
5bb4e73693
|
Review 1
|
2020-07-23 18:49:03 +02:00 |
|
|
Leonardo Alt
|
51721c3080
|
Double SAT run for cex
|
2020-07-23 18:49:03 +02:00 |
|
|
Leonardo Alt
|
694ec92688
|
Generate counterexample message based on cex graph
|
2020-07-23 18:49:03 +02:00 |
|
|
Leonardo Alt
|
744905525f
|
Convert z3 cex graph into STL
|
2020-07-23 18:49:03 +02:00 |
|
|
Leonardo Alt
|
a7a069c74a
|
Refactor constructor exit
|
2020-07-23 18:49:03 +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 |
|
|
chriseth
|
b3566ad0d5
|
Merge pull request #9082 from ethereum/conversionWarnings
Adding `-Wsign-conversion` flag and fixing errors
|
2020-07-13 11:28:09 +02:00 |
|
|
Leonardo Alt
|
88030c6568
|
[SMTChecker] Refactor verification targets
|
2020-07-10 10:28:49 +02:00 |
|
 Alex Beregszaszi
|
a0300835eb
|
Change CHC to avoid sign mismatch
|
2020-07-09 17:22:52 +02:00 |
|
|
Leonardo Alt
|
f97fa9b520
|
[SMTChecker] Add current input variables to the function summary
|
2020-07-02 15:30:29 +02:00 |
|
|
Leonardo Alt
|
5517e817d5
|
Do not trust code of external functions
|
2020-07-01 18:20:46 +02:00 |
|
|
Leonardo Alt
|
56e7d43384
|
Rename var
|
2020-07-01 18:20:34 +02:00 |
|
|
Leonardo Alt
|
5160f89c1b
|
[SMTChecker] Support to external calls to unknown code
|
2020-07-01 18:20:33 +02:00 |
|
  Djordje MijovicandKamil Śliwak
|
c6e4943089
|
Adding fixes for signedness warnings in libsolidity
Co-authored-by: Kamil Śliwak <kamil.sliwak@codepoets.it>
|
2020-06-10 10:41:55 +02:00 |
|
|
Leonardo Alt
|
9e9f0c52e1
|
[SMTChecker] Support to bitwise
|
2020-05-27 20:59:00 +02:00 |
|
|
Leonardo Alt
|
45eba27424
|
Rename namespace
|
2020-05-20 12:55:18 +02:00 |
|
|
Leonardo Alt
|
087605ea02
|
Create libsmtutil
|
2020-05-20 12:55:18 +02:00 |
|
|
Leonardo Alt
|
2435ab938c
|
Add verification target for empty pop
|
2020-05-18 16:35:56 +02:00 |
|
 a3d4
|
8f68c04358
|
Add unique IDs to error reporting calls
|
2020-05-06 13:53:46 +02:00 |
|
|
chriseth
|
41ef13129b
|
Merge pull request #8678 from ethereum/smt_remove_redundant_constraints
[SMTChecker] Remove redundant CHC constraints
|
2020-04-20 15:44:59 +02:00 |
|
|
Leonardo Alt
|
45f22e3ff4
|
Add functional map and fold generic functions
|
2020-04-16 19:21:36 +02:00 |
|
|
Leonardo Alt
|
bca43586c6
|
[SMTChecker] Remove redundant CHC constraints
|
2020-04-15 18:11:39 +02:00 |
|
|
Leonardo Alt
|
e3ec22124e
|
[SMTChecker] Fix ICE in CHC internal calls
|
2020-04-07 01:09:03 +02:00 |
|
|
Leonardo Alt
|
d2f65ea8b1
|
[SMTChecker] Add SortProvider
|
2020-03-26 14:55:54 +01:00 |
|
|
Leonardo Alt
|
07368c2e1e
|
Add support to internal function calls
|
2020-03-11 16:29:07 +01:00 |
|
|
Leonardo Alt
|
3bee348525
|
Change CHC encoding to functions forest instead of explicit CFG
|
2020-03-03 12:12:26 +01:00 |
|
|
Leonardo Alt
|
d31a2a8d21
|
CHC clears indices so that initial is 0 and current is 1
|
2020-02-12 11:47:58 -03:00 |
|
 Christian Parpart
|
6b23412fae
|
C++ namespace cleanup (except tests).
|
2020-01-07 15:51:50 +01:00 |
|
|
Leonardo Alt
|
f4f83690f3
|
Replace some shared_ptr by unique_ptr or raw pointers
|
2020-01-06 14:16:49 +01:00 |
|
|
chriseth
|
f6916a637e
|
Merge remote-tracking branch 'origin/develop' into develop_060
|
2019-12-09 17:16:58 +01:00 |
|
|
Leonardo Alt
|
225041738e
|
Add SMTCheckerTest for isoltest
|
2019-12-09 15:32:08 +01:00 |
|
|
chriseth
|
e061f1e743
|
Merge remote-tracking branch 'origin/develop' into HEAD
|
2019-12-05 16:44:26 +01:00 |
|
|
Leonardo Alt
|
48c3a5c225
|
[SMTChecker] Create options to choose SMT solver in runtime
|
2019-12-04 17:31:44 +01:00 |
|
|
chriseth
|
96d777d7f1
|
Merge commit 'a7d481fb9' into develop_060
|
2019-12-03 20:47:30 +01:00 |
|
|
Leonardo Alt
|
c09da092d2
|
[SMTChecker] Fix constructors with local vars
|
2019-11-29 16:59:15 +01:00 |
|
|
Leonardo Alt
|
a352abe00d
|
[SMTChecker] Add support to constructors
|
2019-11-28 14:43:23 +01:00 |
|
|
Leonardo Alt
|
ddc478e3e4
|
Add CallbackKind and use it for the SMT solver
|
2019-11-21 22:10:21 +00:00 |
|