Currently we compile dynamic dispatch into an explicit switch table inside a special dispatch function. However if the address doesn't match any known contract we abort. This is useful for testing, but for analysis we need to assume that an unknown function that we don't have access to may be called. This can be represented with some form of havoc
Currently we compile dynamic dispatch into an explicit switch table inside a special dispatch function. However if the address doesn't match any known contract we abort. This is useful for testing, but for analysis we need to assume that an unknown function that we don't have access to may be called. This can be represented with some form of havoc