Leo Alt
24df40de9a
Allow running Eldarica from the command line
2022-11-22 21:16:45 +01:00
Leo Alt
75d08ea924
Check early if solvers are available.
2022-05-11 20:02:31 +02:00
Leo Alt
e40cf92b1d
[SMTChecker] Merge all entry points for a target
2021-11-03 11:12:58 +01:00
Leo Alt
49e7627bd3
Use invariants in CHC
2021-10-26 11:30:30 +02:00
Leo Alt
8e81df1bd3
Do not show redundant unsupported errors in SMTChecker
2021-08-27 16:25:09 +02:00
Leo Alt
61160aa0e7
Add constraints correlating address(this).balance and msg.value
2021-08-25 21:10:08 +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
Leonardo Alt
4b2ccf2f37
Abstract function smtchecker natspec
2021-05-11 15:30:19 +02:00
Leonardo Alt
dd1865873e
Choose contracts to be analyzed by the SMTChecker
2021-04-21 10:34:14 +02:00
Leonardo Alt
ba97d6ac4e
Add local vars to cex
2021-03-30 17:55:21 +02:00
Leonardo Alt
dbd067d6db
Report out of bounds index access
2021-03-30 10:28:48 +02:00
Mathias Baumann
e197ebbdd1
Replace TypePointer with Type const*
2021-03-23 11:47:19 +01:00
Leonardo Alt
998346e599
Fix bug in virtual functions called by constructor.
2021-03-12 16:42:28 +01:00
Leonardo
7405dc5b7f
Merge pull request #10836 from ethereum/smt_fix_cex_inheritance
...
Fix inheritance bug in CHC cex
2021-02-03 18:49:25 +01:00
Martin Blicha
f1013427a7
[SMTChecker] refactoring the accessing the encoding state
2021-02-03 15:53:58 +01:00
Leonardo Alt
665ce27c18
Fix inheritance bug in CHC cex
2021-02-02 18:06:32 +01:00
Leonardo Alt
3b23cadbdc
Add CLI and JSON option to select SMTChecker targets
2021-01-20 17:35:37 +01:00
Leonardo Alt
b3c3836388
Output internal calls
2021-01-12 14:57:04 +01:00
Martin Blicha
0f3924186e
[SMTChecker] Support try-catch in CHC engine
2021-01-11 13:36:02 +01:00
Leonardo Alt
11f56861c3
Refactor cex loop
2021-01-07 23:13:02 +01:00
Leonardo Alt
b7ac207391
[SMTChecker] Support return in CHC
2020-12-07 18:17:33 +01:00
Leonardo Alt
7490ffbe13
Use nonlinear clauses instead of inlining for base constructors
2020-12-04 13:25:56 +01:00
Martin Blicha
5ca7a24896
[SMTChecker] Added support for precise modeling of external calls to this.
...
Modeling external calls to this, since we can trust these calls.
fixed problem with transaction data not being restored after trusted external call
update to the tests
additional tests
changelog entry
added tests for external getters of this
2020-11-13 11:49:09 +01:00
Leonardo Alt
646be53f2f
Sort variables and expressions by AST id
2020-11-06 11:50:43 +00:00
Leonardo Alt
d03ddeb0fa
[SMTChecker] User timeout option
2020-11-03 10:46:11 +00:00
Martin Blicha
c1a57ffbfe
[SMTChecker] More precise creation of verification targets.
2020-10-30 19:11:28 +01: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
Martin Blicha
f0d81601db
[SMTChecker] Adding division by zero checks in the CHC engine
2020-10-21 14:48:33 +02:00
Leonardo Alt
18cf01c187
Add this and state to CHC
2020-10-12 11:11:52 +01:00
Leonardo Alt
c8cc73c80c
Support array slices
2020-10-01 11:52:02 +02:00
Leonardo Alt
352cce5fc8
[SMTChecker] Support addmod and mulmod.
2020-09-29 12:45:19 +02:00
Leonardo Alt
3519b38055
Move predicate functions from CHC to PredicateInstance
2020-09-28 12:43:19 +02:00
Leonardo Alt
ac93ee1d08
Move error flag from CHC to SymbolicState
2020-09-28 12:37:57 +02:00
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
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
Leonardo Alt
8a06041bbe
[SMTChecker] Add underflow/overflow target to CHC
2020-08-14 12:58:27 +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
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
Leo Alt
chriseth
Mathias Baumann
Martin Blicha
Martin Blicha
Sachin Grover