search

microsoft / verisol

A formal verifier and analysis tool for Solidity Smart Contracts
Other
245 stars 46 forks source link

Shuvendu fallback #186

Closed shuvendu-lahiri closed 5 years ago

shuvendu-lahiri commented 5 years ago

Address #4, #90, #137, #146.

  1. Models fallbacks
  2. Models send
  3. Models transfer
  4. Do not catch exception for send
  5. Do not model gas limit for send/transfer
  6. Support for foo.value(x)(args) or foo.value(x).gas(y)(args)
  7. Support for call.value(x).("") for invoking fallback
  8. Call to a fallback of an unknown contract (code not present) will cause all globals to be havoced