Idea : Documenting and checking the invariants on goto programs

[martin-cs]

[ Documenting a TODO : Thanks to @thk123 for the prompt, @smowton and @jgwilson42 for previous discussions and @peterschrammel for ideas. ]

There are a number of obvious and less obvious invariants on goto-programs and what "well structured" means. At the moment these are at the stage of fokelore with scraps being documented, which is not exactly an ideal state of affairs. Maybe we could...

1. Write an is_valid() method for goto_functionst and goto_programt which checks if it is well structured. As @peterschrammel observes, there are various, nested correct forms (have function pointers been removed, have throw/catch been removed, etc.) so it might be good to take parameters to denote which form it should be in.

2. Add in assert(program.is_valid()) calls at key locations, including after the front-end / load from file, after instrumentation passes and before the back-end engines.

3. If you want to assume something about the structure of a program, add to the validity check, get it merged and assume away.

@peterschrammel adds:

There are several kinds of Goto program that (should) form a subset chain. The transformations in process_Goto_program() go through this chain in several feature reduction passes. Certain analyses may require a specific kind of Goto program. So, 'valid' depends on the stage of processing. We should make this explicit.

[tautschnig]

Closing as I believe this is now done.