Cleanup/refinement of goal tags

[robdockins]

PR #1679 adds features for tagging goals to help with proof readability and robustness. This ticket exists to track some remaining questions and cleanup related to this feature.

1. I implemented most of what's needed for JVM use of this feature, but have not tested it at all. We should run the new feature through its paces in JVM and add at least a basic unit test.
2. I added an option to allow "special case" handling when only a single override applies at a call site, but only for LLVM. Is this feature useful? Should it be configurable? Do we need a more precise way to specify when it should be enabled (e.g., per override, per call site, etc.)
3. The JVM and X86 verifiers do not implement the special case, and perhaps they should.
4. execute_func and return specification statements currently do not capture tag values, and they probably should.
5. A single atomic specification statement (e.g. points-to) may generate more than one proof goal, so tag values may not be enough to uniquely specify a proof goal of interest. This might force users to fall back on the goal numbering to pick out a particular goal that requires special handling, which is undesirable. We should find some way that users can uniquely specify a goal of interest using some combination of tags and other metadata to avoid relying on fragile goal numbering.

[robdockins]

Another thought: we should also expose goal tags via the Python interface.