This is common with C, when interfacing with hardware.
What exact C code did you had in mind?
So that the counter example is close enough to it in exposing the same semantics.
This is common with C, when interfacing with hardware.