Unit/regression tests for vtable size and align fields

[avanhatt]

We should have tests that check that the vtable size and align fields that we generate match:

1. The rustc vtable implementation.
2. The CBMC size_of_* function results.