Improved stack identification, many other changes

[l-kent]

A number of changes here that cause many more test cases to pass than before.

• Better stack identification
• All registers are now global variables in Boogie and not passed as parameters
• Correct modifies clauses are now generated
• Boogie-level specifications can now be added to specification files (this is basically a temporary measure pending a more extensive rewrite of the specification system)
• The case where the 'main' procedure is optimised out is now handled, with a 'mainProcedure' field in the Program class used to denote the initial procedure instead of just matching on the name
• Assertions with comments have been added to the IR
• Specifications now support specifying the security level for a whole array properly
• Renaming all the parsing-related classes to be more relevant
• .got and .rodata memory sections have been added to the initialised memory

[l-kent]

Are you able to review this @ailrst?

[ailrst]

LGTM 🚀