Spurious warning messages in generated code

[alastairreid]

Motivation

Some tools (compilers, formal verification tools) generate a lot of spurious warning messages because of how our code generator works.
These are unsettling for users of the code and, because we respond by disabling many warnings, it may lead to genuine issues being missed.

Some of the issues are

• Including unnecessary parentheses - especially around equality checks "(x == 42)"
• Inserting dead code
  - [ ] Default cases in exhaustive switch statements (e.g., when all values of an enumerated type are covered)
  - [ ] Dead variables (or, rather, variables that are written to but not read from)
  - [ ] Possibly: unused variables
  - [ ] Possibly: unused functions