Last week I spent a little bit of time making internal information from cXprop available to Will Archer for use in his Caduceus-using tool. Unfortunately, I came at the problem with the wrong set of assumptions and it has ground the idea to a temporary halt. Hopefully we can resolve the issues during our group meeting on Thursday.
My faulty assumption was that cXprop was going to be used on whole-program code, and probably on TinyOS code. Although it works on other things, that is normally the target. It turns out Will is using it on single files that may or may not have anything to do with TinyOS. This means that I do not know any order of execution inside the functions, so I basically have to assume ALL orders of execution.
The problem is that this model does not exist in cXprop, except for interrupts. I would have to adapt that model to functions in files. Which should not be too hard, but John wants me to stop hacking on code and keep working on my "critical path" writing/presenting projects. Which is why I have not actually done it yet. There might also be little nuances I have not thought of yet. Until I create this model, Will uses a version that assumes "bottom" for incoming entry-point function state, which basically means nothing gets learned.
Entry-point functions are defined as those which are visible outside the file. This essentially means anything not labeled as static, although there are a few other less-common cases.