cerc-io/solidity
10
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,792 Commits 348 Branches 121 Tags 100 MiB
a4d777643d
Commit Graph

30 Commits

Author SHA1 Message Date
Nikola Matic
d0a5556fd0 Purge using namespace from libsolidity/formal 2023-08-15 14:40:27 +02:00
Leo Alt
aacbe72079 group unsupported warnings 2023-03-15 17:06:06 +01:00
Leo Alt
21c0f78650 Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
Leo Alt
24df40de9a Allow running Eldarica from the command line 2022-11-22 21:16:45 +01:00
Marenz
f7cc29bec1 Add std:: qualifier to move() calls 2022-08-30 11:12:15 +02:00
Leo Alt
8e81df1bd3 Do not show redundant unsupported errors in SMTChecker 2021-08-27 16:25:09 +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
dd1865873e Choose contracts to be analyzed by the SMTChecker 2021-04-21 10:34:14 +02:00
Leonardo Alt
b753cb6120 Deprecate pragma experimental SMTChecker 2021-04-08 21:03:38 +02:00
Leonardo Alt
3b23cadbdc Add CLI and JSON option to select SMTChecker targets 2021-01-20 17:35:37 +01:00
Daniel Kirchner
7308abc084 Allow loading Z3 dynamically at runtime. 2020-12-10 16:47:47 +01:00
Leonardo Alt
d03ddeb0fa [SMTChecker] User timeout option 2020-11-03 10:46:11 +00:00
Leonardo Alt
4e49135318 Add CLI option to choose model checker engine 2020-10-16 15:01:47 +01: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
88030c6568 [SMTChecker] Refactor verification targets 2020-07-10 10:28:49 +02:00
Leonardo Alt
45eba27424 Rename namespace 2020-05-20 12:55:18 +02:00
Leonardo Alt
3bee348525 Change CHC encoding to functions forest instead of explicit CFG 2020-03-03 12:12:26 +01:00
Christian Parpart
6b23412fae C++ namespace cleanup (except tests). 2020-01-07 15:51:50 +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
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
4214cd1354 [SMTChecker] Fix ICE when reporting cex concerning state vars from different source files 2019-08-10 20:56:52 +02:00
Leonardo Alt
03cc124f32 Add CHC skeleton 2019-07-19 11:52:05 +02:00
Leonardo Alt
01570bbc8c EncodingContext's solver needs to be set dynamically 2019-07-08 14:40:15 +02:00
Leonardo Alt
3cb4ed83c1 [SMTChecker] Split SMTChecker into SMTEncoder and BMC 2019-07-01 15:05:03 +02:00