Closed
Description
Main design goals of:
- context insensitivity (there is one summary applicable in any context the function is called from)
- transitive closure (effects of all callees are captured in summaries of the root caller function)
- generalised interface (suitable for many different concrete summary-computing algorithms)
- language independent (should work for Java, C, C++, ...)
Known links to other tasks/projects:
- test_gen (our summaries should fit to needs of this tests generation task)
- 2ls (their summaries should also be expressible in our summaries)
- path-symex (summaries must also be usable for path-based symbolic execution)
Method:
I'll iteratively improve the structure of the summaries. I'll start with a simple implementation tested on few hand-written benchmarks and then I'll discuss the design of summaries with others (mainly from the related projects) to get a feedback. In each subsequent iteration I'll update the implementation according the the feedback from the previous iteration. I expect two or three iterations until the summaries will be ready to tackle real-world programs. An iteration may approximately take one week.