Remove speculative features from specification

[dtarditi]

The following features are speculative and should be removed from the specification. They can be placed in a separate TeX file for future use/reference:

• Definite initialization analysis. Given that widely used C compilers like clang and GCCC now have flags that initialize automatic variables to 0, this seems like it isn't worth the effort.
• Opaque types: this is an idea of allowing typedefs to define abstract types, instead of being transparent. It is a nice idea, but we don't have the resources to do this.
• Undefined behavior in C11 for misaligned pointer types. We don't have the resources to do this right now.

[dtarditi]

This is in-progress: see this branch: https://github.com/checkedc/checkedc/tree/checkedc-v1.