ChenfengWei0 / esbmc

The efficient SMT-based bounded model checker

http://esbmc.org/

Other

0 stars 1 forks source link

[Solidity] TODO #8

Open ChenfengWei0 opened 9 months ago

ChenfengWei0 commented 9 months ago

bug fix
- state var name
- "is" keywords
- contract mode when functions have arguments
- byte array index out of bound check
- function mode: constructor call
- k-induction ...
multiple return(tuple)
- First we need to implement the tuple in c++
pure/view/calldata/event/emit keywords
built-in properties(SO MANY!!!)
Extend verification to recursive
performance boost up.

ChenfengWei0 commented 8 months ago

defualt value

ChenfengWei0 commented 6 months ago

refactor the find id. the reference_id == "#id"

ChenfengWei0 commented 6 months ago

todo for Christmas

Modifier
Struct
Map