Martin Blicha
12bca24774
[SMTChecker] Use path condition when creating CHC targets
...
Without path condition, verification targets created inside ternary
operator ignore the condition of the operator inside the branches.
This led to false positives.
Further updates:
- Function calls should consider the conditions under which they are
called, otherwise the analysis may report false positives.
The fix proposed here is to add the current path condition to the edge
that propagates error from a function call.
- Increment error index after function call
This is necessary for the analysis of the ternary operator to work
correctly. No information should leak from a function call inside a
ternary operator in the first branch to the second branch, including
whether or not an error would have occured in the first branch.
However, for the execution that continues after the function call,
we still need to ensure that under the current path condition
the error has not occurred in that function call.
It would be better to isolate the analysis of the branches to separate
clauses, but I do not see an easy way for that now. In this way, even
though the function call in first branch is included in the clause of
the second branch, no information leaks.
- Additonal test for ternary operator
This tests the behaviour of SMTChecker on ternary operator with function
calls inside both branches. Specifically, it tests that SMTChecker
successfully detects a violation of a verification target in the second
branch when the same target is present also in the first branch, but
there it cannot be triggered because of the operator's condition.
2023-04-21 18:56:34 +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
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
a5dab6181c
Fix internal error when the abstract-nondet SMTChecker natspec annotation is used with a wrong option multiple times for the same function
2022-11-28 16:59:35 +01:00
Leo Alt
9a8dd4242f
Fix SMTChecker bug when a public library function is called internally by an internal library function, which in turn is called internally by a contract.
2022-11-28 13:07:18 +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
75d08ea924
Check early if solvers are available.
2022-05-11 20:02:31 +02:00
Tyler
047034544e
Merge branch 'develop' of github.com:tfire/solidity into fix/remove-namespace-ast-annotations
2022-03-09 18:55:22 -05:00
Tyler
519e1c9402
Specify namespaces
...
Fix references into solidity::util
2022-03-08 00:09:17 -05:00
wechman
52dfccca98
Replace all locale-dependent operations with locale-agnostic counterparts
2022-03-07 17:23:08 +01:00
Leo Alt
fb8c138b8b
Do not analyze unecessary contracts
2021-12-24 19:36:32 +01:00
Leo Alt
16535aae32
Fix ICE when unsafe targets are solved more than once and the cex is different
2021-12-03 00:21:38 +01:00
Leo Alt
dff280cadc
Fix ICE in CHC when using gas in the function options
2021-11-03 15:40:54 +01:00
Leo Alt
e40cf92b1d
[SMTChecker] Merge all entry points for a target
2021-11-03 11:12:58 +01:00
Leo Alt
d419c30ca6
Add errorCode list to invariants report
2021-10-26 11:30:30 +02:00
Leo Alt
49e7627bd3
Use invariants in CHC
2021-10-26 11:30:30 +02:00
tcoyvwac
ba0c09e082
Prefer make_unique over new
2021-10-15 19:46:47 +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
Leo Alt
106c591dde
Support the external call option
2021-09-01 20:18:37 +02:00
Leo Alt
60b866f9d8
Fix ICE on multi-source use of abi.*
2021-08-27 18:55:36 +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
a55685c04f
Erase balances when delegatecall is seen
2021-08-25 12:39:26 +02:00
Leo Alt
d89d63bf9c
Use the nondeterministic interface also for BARECALL
2021-08-19 16:34:01 +02:00
Leo Alt
6ee60aa628
Fix false positive on external calls from constructors
2021-08-12 18:51:55 +02:00
Leo Alt
10397e440c
Fix ICE in constants
2021-08-12 10:53:01 +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
Leo Alt
547a6915ad
Fix ICE on external calls from constructor
2021-06-01 14:21:48 +02:00
Leo Alt
f7b045b886
review
2021-05-26 22:12:49 +02:00
Leo Alt
daea5f886d
Fix CHCSmtLib2Interface
2021-05-26 22:12:49 +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
095d337140
Basic support to free constants
2021-04-19 19:23:18 +02:00
Leonardo Alt
4e34359063
Basic support to free functions
2021-04-19 19:23:18 +02:00
Leonardo Alt
b753cb6120
Deprecate pragma experimental SMTChecker
2021-04-08 21:03:38 +02:00
anurag4u80
bbcdddeed9
Replaced keys, values and reverse with ranges
2021-03-31 23:33:04 +05:30
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
Leonardo Alt
d1db41a5c8
Fix target warning order nondeterminism
2021-03-26 12:13:52 +01:00
Martin Blicha
85358dfe30
[SMTChecker] Do not create targets for contracts that cannot be deployed
2021-03-25 15:38:37 +01: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 Alt
6fd76e830d
Fix CHC cex order
2021-03-11 10:36:40 +01:00
Martin Blicha
4285c2803b
[SMTChecker] Fix ICE on array.pop nested inside 1-tuple
2021-03-09 20:00:51 +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
