> You could do this with the C abstract machine.

I don't think there is a "C abstract machine". I think there are some, like, minimal versions of C (there's probably a Featherweight C out there or something), but the C specification is not given in terms of an abstract machine, and any abstraction of the machinery of C will necessarily lose important implementation details (e.g., undefined or unspecified behaviors, for instance).