I have an Uno R3. I have timer 1 set to CTC mode with OCR1A being used for TOP. OCR1A = 0xFFFF. The prescaler is set to 1024. OCR1B = 0x7FFF and the interrupt bit for it is set. When its interrupt triggers, the LED gets toggled.
TCNT1 is the same IO address as TCNT1L so it prints just the lower byte of the counter. If you first assign the value to an uint16_t typed variable you probably get better results.
The code does compile in C++14 and after (cppreference).
Turns out that init() (which is called by main()) sets bit 0 of TCCR1A. Because I set bit 3 in setup(), timer 1's mode is set to Fast PWM with TOP at 0x00FF. This explains why it clears at 255. Setting TCCR1A to 0 fixes the issue. I'll be writing my own main() from now on.
The compiler automatically deals with accessing TCNT1 in C/C++ code. From the datasheet:
Note that when using “C”, the compiler handles the 16-bit access.
Feel free to repeat errors that have been found by many other coders before you.
Feel free to ignore the great Arduino framework and examples and bypass it by your own buggy code.