it's a little weirder though.
int main(int argc, char argv)
{
int a = 0;
printf("%i %i %i\n", a, a++, a++);
}
will give "0 0 1" (gcc 4.2.1), the increment "shouldn't" happen until after the ; if you're going with post statement. I think your rule would expect "0 0 0" with a being 2 after the printf.
BUT! you get a warning, so that's nice.