[c] 'printf' with leading zeros in C

Your format specifier is incorrect. From the printf() man page on my machine:

0 A zero '0' character indicating that zero-padding should be used rather than blank-padding. A '-' overrides a '0' if both are used;

Field Width: An optional digit string specifying a field width; if the output string has fewer characters than the field width it will be blank-padded on the left (or right, if the left-adjustment indicator has been given) to make up the field width (note that a leading zero is a flag, but an embedded zero is part of a field width);

Precision: An optional period, '.', followed by an optional digit string giving a precision which specifies the number of digits to appear after the decimal point, for e and f formats, or the maximum number of characters to be printed from a string; if the digit string is missing, the precision is treated as zero;

For your case, your format would be %09.3f:

#include <stdio.h>

int main(int argc, char **argv)
{
  printf("%09.3f\n", 4917.24);
  return 0;
}

Output:

$ make testapp
cc     testapp.c   -o testapp
$ ./testapp 
04917.240

Note that this answer is conditional on your embedded system having a printf() implementation that is standard-compliant for these details - many embedded environments do not have such an implementation.