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
f9fa76c9d3
smt encode call
2022-04-11 12:19:41 +02:00
Daniel Kirchner
0f1a63c3fa
Fix import directive visits in type checker and view pure checker.
2022-03-14 14:53:06 +01:00
Tyler
519e1c9402
Specify namespaces
...
Fix references into solidity::util
2022-03-08 00:09:17 -05:00
nishant-sachdeva
9043621747
Changed occurences of isByteArray() to isByteArrayOrString(). The idea
...
is to, in a future commit, replace such occurences of
isByteArrayOrString() which are required to return True only for Bytes
type with a new isByteArray() function.
2022-02-02 14:19:58 +05:30
Leo Alt
fb8c138b8b
Do not analyze unecessary contracts
2021-12-24 19:36:32 +01:00
Marenz
7a96953e78
Implement typechecked abi.encodeCall()
2021-12-16 17:35:58 +01:00
Leo Alt
316be7206f
Fix soundness of storage/memory pointers that were not erasing enough knowledge
2021-12-14 12:02:18 +01:00
Leo Alt
d81ebe97c3
Fix magic access
2021-10-01 12:57:06 +02:00
chriseth
1531863835
Split Common.h into Numeric.h.
2021-09-23 15:27:29 +02:00
Leo Alt
e74f853c6b
[SMTChecker] Support user types
2021-09-21 13:23:17 +02:00
Leo Alt
a1bea368cb
[SMTChecker] Support constants via modules
2021-09-16 14:35:05 +02:00
Leo Alt
6e2fe1e340
[SMTChecker] Cleanup spurious messages about TypeTypes
2021-09-07 16:55:25 +02:00
Leo Alt
106c591dde
Support the external call option
2021-09-01 20:18:37 +02:00
Marenz
2b28f87abf
Add type().min/max for enums
2021-09-01 15:02:02 +02:00
Leo Alt
16bc15acac
Fix false negative on storage array references returned by internal functions
2021-08-28 09:30:53 +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
Leonardo
6e6bbb2f83
Merge pull request #11837 from soroosh-sdi/use-range-v3-part2
...
Using range-v3 instead of boost
2021-08-26 09:38:27 +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
soroosh-sdi
b0ce98bcb2
Using range-v3 instead of boost
...
Signed-off-by: soroosh-sdi <soroosh.sardari@gmail.com>
2021-08-24 23:50:23 +04:30
Leo Alt
d89d63bf9c
Use the nondeterministic interface also for BARECALL
2021-08-19 16:34:01 +02:00
Leo Alt
10397e440c
Fix ICE in constants
2021-08-12 10:53:01 +02:00
Leo Alt
08c065ee04
Add option divModWithSlacks
2021-08-06 15:50:25 +02:00
chriseth
e3525b81d0
Supply scanner to model checker.
2021-07-14 15:12:10 +02:00
Leo Alt
bf21cd400c
Fix conversion from bytes to fixed bytes
2021-06-01 17:55:18 +02:00
Leo Alt
95f973e08a
Fix gasleft variable name
2021-05-26 22:12:49 +02:00
Martin Blicha
9c98ab59f0
SMTChecker: fixed struct constructor where FixedBytes member is initialized with a string literal
2021-05-17 13:52:37 +02:00
Leonardo Alt
4b2ccf2f37
Abstract function smtchecker natspec
2021-05-11 15:30:19 +02:00
Leo Alt
e2959ce55c
Assign cast from constants directly
2021-05-11 14:07:09 +02:00
Leo Alt
1642c10f6e
Fix ICE in free functions
2021-05-03 10:57:11 +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
chriseth
98a8640928
Merge pull request #11203 from anurag-git/issue_10738-1
...
Use range-v3 loops (reverse, keys, values)
2021-04-01 12:19:40 +02:00
anurag4u80
bbcdddeed9
Replaced keys, values and reverse with ranges
2021-03-31 23:33:04 +05:30
Martin Blicha
330fb8f4d0
[SMTChecker] Assignment refactoring
2021-03-31 13:36:50 +02:00
Leonardo
78d94737a4
Merge pull request #11188 from blishko/issue-11181
...
[SMTChecker] Fix crash when analysing try-catch clauses with function call.
2021-03-31 11:24:36 +02:00
chriseth
b04b189959
Syntax for custom errors.
2021-03-30 21:15:18 +02:00
Martin Blicha
2d231f1859
[SMTChecker] Changed SMTEncoder::mergeVariables to work regardless which branch has been visited first
2021-03-30 20:35:44 +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
Martin Blicha
5293f05ee3
[SMTChecker] Fix ICE on ABI functions with no arguments
2021-03-25 13:28:29 +01:00
Martin Blicha
98446782e2
[SMTChecker] Fix compound assignment to push
2021-03-24 14:54:13 +01:00
Martin Blicha
852e877ae7
[SMTChecker] Handle InaccessibleDynamicType
2021-03-24 11:53:06 +01:00
Mathias Baumann
e197ebbdd1
Replace TypePointer
with Type const*
2021-03-23 11:47:19 +01:00
Leonardo
25b31111df
Merge pull request #11040 from ethereum/smt_fix_virtual_one_more_time
...
[SMTChecker] Fix bug in virtual functions called by constructor
2021-03-17 16:54:36 +01:00
Martin Blicha
432944d0b4
[SMTChecker] Small refactoring of defining SMT expressions for structs/tuples
2021-03-16 15:34:43 +01:00