Audit Vtable generation for dynamic traits

[danielsn]

RMC handles dynamic traits by making a vtable for each trait, which maps virtual calls to the function pointer that implements the call. As of 2021-09-01, our implementation of dynamic traits has no known soundness issues.

Likelihood:

Due to the complexity of this feature, there may be currently-unknown soundness issues.

Mitigation:

• The default flags RMC passes to CBMC now include --pointer-check, so incorrect codegen of functions is now more likely to be found a verification time.
• We have added 40+ regression tests for dynamic traits.