Expressions in the programming language C have such an under-specied semantics that one might expect them to be non-deterministic. However, with the help of a mechanised formalisation, we have shown that the semantics’ additional constraints actually result in a large class of C expressions having only one possible behaviour.