Exporting function frame information

[travitch]

Some potential users of our tool would find it very useful to be able to consume the function-level pre- and post-domain information we are generating. We need to export this in a form that is easily consumable. Some examples that have come up in conversation so far include:

• [ ] For pointer arguments, report how many bytes are accessed through them; this will help with stack symbolization and aid in reasoning about how much of the stack is escaping with each local pointer passed to callees. For example, in a call to foo(int *p), it would be important to know if 4 bytes are ready through p (i.e., it points to a scalar), or if a larger (potentially symbolic) number of bytes represent an array on the stack).
• [ ] Similarly, it would be useful to know if a pointer is never dereferenced, indicating that it may be a sentinel pointer marking the end (or one past the end) of a data structure
• [ ] Relational constraints capturing pointers used as upper or lower bounds for a range of addresses (this might be part of a general facility for describing relational bounds that could also include array length arguments)