stack/printf/va_arg Problem bei arm-none-eabi-gcc und STM32

Hallo,

mein Kollege und ich versuchen seit mehreren Tagen ein seltsames Problem 
zu fixieren:

Umgebung:
  STM32F103 mit arm-none-eabi-gcc (mit 4.6 und 4.7 bereits probiert)

Code (nur Prinzip):

1

void interrupt_1ms()

2

{

3

  printf("%f",1.234);

4

}

5

6

void test()

7

{

8

  // irgendwas

9

}

10

11

void main()

12

{

13

  while(1)

14

  {

15

    test();

16

  }

17

}

Symptom:
Meistens wird 1.234000 durch den printf erzeugt (und über RS232 
ausgegeben), und manchmal 0.000000. Wird test(); nicht aufgerufen, passt 
alles.

Ein Versuch printf selbst nachzuprogrammieren (unter Verwendung von 
va_arg) hat zu dem selben Ergebnis geführt. Es stimmen einfach manchmal 
die von va_arg zurückgegebenen Werte nicht wodurch printf ebenfalls 
seine Probleme hat.

Im Internet gefundene Lösungsvorschläge wie
http://www.coocox.org/forum/topic.php?id=346
haben das Problem nicht gelöst.

Unsere Vermutung ist, dass irgendwo das stack alignment sich nicht mit 
va_arg verträgt.

Hat jemand von euch dieses Problem auch schon gehabt und eine Lösung 
dazu finden können. Ich kann mir nicht vorstellen, dass printf einfach 
nicht gehen.

Besten Dank.

mfg, Weinga-Unity