Enforce effective types for specified-width integer types

[btj]

VeriFast accepts the following program, even though it exhibits undefined behavior per C's "effective types" rules:

#include <stdlib.h>
#include <stdint.h>

int main()
//@ requires true;
//@ ensures false;
{
  int i = 0;
  int *p = &i;
  int16_t *q = (void *)p;
  *p = 42;
  //@ open integer(p, 42);
  //@ open int_(p, some(42));
  //@ integer__to_chars(p, 4, true);
  //@ chars_to_integer_(q, 2, true);
  *q = 0; // This is Undefined Behavior. It can lead to miscompilation: https://godbolt.org/z/Yz6z1G6f5
  abort();
}

See #315 .