Incorrect output when using printf and float in interrupt handler with SDK 1.4

[mk-fhg]

The following minimal working example breaks when switching form SDK release 1.3.1 to 1.4:

#include <stdio.h>
#include "pico/stdlib.h"

#define PIN_INTERRUPT 22

void isr()
{
    float foo = 123.4567;
    int   bar = 42;
    irq_clear(IO_IRQ_BANK0);
    printf("isr_foo = %f\n", foo); // Prints as "isr_foo = -0.000000"
    printf("isr_bar = %d\n", bar); // Prints as "isr_bar = 42"
}

int main()
{
    stdio_init_all();
    gpio_init(PIN_INTERRUPT);
    gpio_set_dir(PIN_INTERRUPT, GPIO_OUT);
    gpio_set_irq_enabled_with_callback(PIN_INTERRUPT, 0x00000008, true, isr);
    
    while(1)
    {
        float foo = 123.4567;
        printf("main_foo = %f\n", foo); // Prints as "main_foo = 123.456703"
        
        gpio_put(PIN_INTERRUPT, 1);
        gpio_put(PIN_INTERRUPT, 0);
        sleep_ms(1000);
    }
    return 0;
}

With SDK release 1.3.1 prinf works as expected. When using release 1.4 printf outputs an incorrect value when used with a float variable and called from an interrupt handler. In this example the incorrect output is -0.000000. In the original code where I noticed this error first and from which I derived the example above, the output changed from call to call and was one of the following values:

• -2.682e154
• -2
• -0.000
• 0.000
• 2
• 2.682e154