Configurability of Analysis

[Baltoli]

Currently, the analysis written is completely specific to the one automata developed. A big improvement to this framework is probably to work out how this can be effectively generalised to arbitrary automata (though the hard-coded approach remains useful as a proof-of-concept that this sort of thing is useful, and could be used on actual examples).

Things to think about:

• Analysis of manifest structures in more depth, and looking for substructures that can be matched or statically analysed (e.g. a sequence of calls).

[Baltoli]

A simple example case might be sequencing of two or more function calls - this could be statically checked at the IR level reasonably easily.

[Baltoli]

A big thing to think about is how to compose static analyses of an assertion - it's very easy to write an analysis for a simple case, but how could a generic framework be implemented?

A system for composing static analyses would be a really useful thing to have, even if it were on a limited part of the assertion grammar.

One way to possibly look at this is from the perspective of each assertion grammar construct in a general way - what program properties do they enforce?

Is it possible to delete subcomponents of an automaton?

[Baltoli]

This is covered by #50 - I think that's probably the generic & composable approach that we're looking for.