On: A semantic model for a substantial fragment of C

[fmap]

I'm not sure about non-deterministic behavior without looking it up, but you can fix this example to be implementation defined, rather than undefined like this:

  #include <stdio.h>
  
  int postincrement(int *x) { int y = *x; *x = y + 1; return y; }
  
  int main(int argc, char **argv) {
    int i = 0;
    printf("%d, %d\n", postincrement(&i), postincrement(&i));
    return 0;
  }

The point is that function arguments introduce sequence points, but the specification for i++ is weaker than what you get for a function call. C is full of gotchas like this...