AVR-GCC for Linux doesn't handle well 16 bit words

My problem is that I'm using a real time kernel that includes its own tick counter, so I can't (yes, I can but I shouldn't) mix counters.