Use structured symbolic storage with symbolicStorage
/--symbolic-storage
#577
Labels
enhancement
New feature or request
symbolicStorage
/--symbolic-storage
#577
PR #571 by @anvacaru adds support for preserving storage fields in otherwise symbolic storage for contracts during CSE. As discussed today, we can perhaps do the same thing when making contracts' storage symbolic during the execution; it is currently done via
symbolicStorage(address)
cheatcode, but it might be easier to do through introducing a CLI argument--symbolic-storage
— that would probably mean that all contracts getting deployed during the execution would have symbolic storage by default.That would make constraints more compact and readable as that'll substitute, e.g.,
SF_C:Int
instead of#lookup ( CONTRACT_STORAGE:Map , 0 )
, which might bring usability and performance improvements. That would, however, require extending support for more storage field types than is present in #571.The text was updated successfully, but these errors were encountered: