Analysing contract permissions using symbolic analysis and decompiled sources - example

Hi all,
We just hacked a proof of concept tool for finding addresses that are being referenced by a smart contract:

It uses API from the symbolic decompiler to figure out stuff like this:

If anyone’s interested in how it’s done, you can check the github for sources, and also the intermediate language form that is the basis for the analysis, available here: