I found out that the ARM-compiler armcc V5.05 does not compile uint64_t correctly into assembly code. It uses only one register instead of two so the result is truncated to 32 bits (though the compiler is not complaining).
As a workaround I used the gcc compiler, put the generated assembler code into a separate asm file and ran the ARM assembler. The target could not be created due to the error:
This register combination results in UNPREDICTABLE behaviour
which is really fatal, I suppose. After the C- "return" statement at the end of a function gcc inserts an offending SUB SP,R11,#0 or ADD SP,R11,#0 command before the ASM-return command BX LR. This is true with or without uint64_t.
Can I rely on gcc or is it a bug in armcc/armasm?