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 |
|
Leo Alt
|
0cc9162fb5
|
Update SMTChecker tests
|
2021-08-27 16:25:09 +02:00 |
|
Leo Alt
|
9ea4576664
|
Update tests
|
2021-08-19 16:34:01 +02:00 |
|
Leonardo Alt
|
0a4afa71bd
|
Update old tests
|
2021-04-08 21:03:39 +02:00 |
|
Leonardo Alt
|
50be39fc21
|
Add and update tests
|
2020-12-17 14:42:49 +01:00 |
|
Leonardo Alt
|
80e85b772b
|
[SMTChecker] Apply const eval to arithmetic binary expressions
|
2020-12-16 14:58:00 +01:00 |
|
Leonardo Alt
|
3c142e0e94
|
Move CHC counterexamples to primary location
|
2020-12-09 19:55:18 +01:00 |
|
Leonardo Alt
|
00858c0ccf
|
Isoltets SMTChecker option and BMC specific tests
|
2020-11-06 15:03:38 +00:00 |
|
Leonardo Alt
|
daf859c15b
|
[SMTChecker] report SMTEncoder warnings also via CHC
|
2020-11-03 16:06:17 +00:00 |
|
Alex Beregszaszi
|
fedbea46cd
|
[SMTChecker] Support type conversions
|
2020-10-02 10:26:02 +02:00 |
|
Leonardo Alt
|
e6bd18525b
|
[SMTChecker] Add engine prefix to verification target error messages
|
2020-09-25 19:09:06 +02:00 |
|
Alex Beregszaszi
|
6edfdff187
|
[SMTChecker] Do not warn on "abi" as an identifer
There is an approprate warning for the function call.
|
2020-09-24 13:57:42 +01:00 |
|
Leonardo Alt
|
00f6b303b1
|
[SMTChecker] Change warning message
|
2020-09-09 16:14:21 +02:00 |
|
Leonardo Alt
|
afcd44e77c
|
Update current tests
|
2020-09-03 15:19:03 +02:00 |
|
Leonardo Alt
|
0a160b1ba0
|
Update remaining tests
|
2020-08-14 12:58:27 +02:00 |
|
Leonardo Alt
|
9d2a0947e9
|
Fix 1-tuple chain
|
2020-07-23 13:46:41 +02:00 |
|
chriseth
|
9743390a53
|
Update tests.
|
2020-07-07 12:16:18 +02:00 |
|
a3d4
|
e04cedafc5
|
Added error codes to SyntaxTest expectations (updated tests)
|
2020-06-22 16:51:47 +02:00 |
|
chriseth
|
96d777d7f1
|
Merge commit 'a7d481fb9' into develop_060
|
2019-12-03 20:47:30 +01:00 |
|
Leonardo Alt
|
a352abe00d
|
[SMTChecker] Add support to constructors
|
2019-11-28 14:43:23 +01:00 |
|
Erik K
|
94272d44aa
|
Merge pull request #7745 from ethereum/develop
Merge develop into develop_060
|
2019-11-19 15:30:31 +01:00 |
|
Leonardo Alt
|
d818746e0c
|
[SMTChecker] Fix ICE in abi.decode
|
2019-11-18 13:15:10 +01:00 |
|
Daniel Kirchner
|
3321fc56ea
|
Split fallback function and introduce "fallback()" and "receive()" syntax.
|
2019-11-04 17:17:58 +01:00 |
|
Leonardo Alt
|
360f868836
|
[SMTChecker] Fix literal string type mismatch
|
2019-08-10 21:51:46 +02:00 |
|
Leonardo Alt
|
fb3c85633b
|
Always create symbolic expression
|
2019-07-01 16:25:33 +02:00 |
|
Leonardo Alt
|
3cb4ed83c1
|
[SMTChecker] Split SMTChecker into SMTEncoder and BMC
|
2019-07-01 15:05:03 +02:00 |
|
Leonardo Alt
|
48d6729164
|
[SMTChecker] Remove overflow check for assignments
|
2019-06-24 17:58:56 +02:00 |
|
Leonardo Alt
|
60a4f03d3d
|
[SMTChecker] Fix ice in unsupported functions with multi return values
|
2019-05-16 18:23:42 +02:00 |
|
Leonardo Alt
|
6027383ae5
|
[SMTChecker] Fix call to function at state var init
|
2019-05-09 16:12:44 +02:00 |
|
Leonardo Alt
|
3d52a6ca68
|
[SMTChecker] Fix ICE in branch-inline function call-modify local variable
|
2019-05-09 09:15:11 +02:00 |
|
Leonardo Alt
|
0b046897ae
|
[SMTChecker] Fix unsupported type assignment
|
2019-05-08 14:28:23 +02:00 |
|