I am not looking for a correction, just an explanation. In the snippet below, why am I getting the output as 2.000000?

#include <stdio.h>
#include <stdlib.h>

int main() {
    double static const val = 0x1P1;
    printf("%d\t%f\n", val, val);
    return EXIT_SUCCESS;
}

Shouldn’t this be equal to 11?