printf: should %f round ???

[Alan Myrvold]

Under Turbo C version 1.5, the statement:
   printf("%14.12f\n",1.0e-12);
produces the curious (and painful) result:
   0.000000000000
Probably because 1.0e-12 is stored inexactly as a number just smaller
that 1.0e-12 and printf is truncating the number to the precision
specified.

I feel deeply that the only REASONABLE behaviour for printf is to
round to the precision specified - but is this behaviour spelled
out anywhere? I looked in my Turbo C manual and K&R 2nd edition
and it seems like the behavour is unspecified. Does anyone
know whether or not the behaviour IS specified?

For completeness, let me note that the following program:

#include <stdio.h>

main()
{
/* 1 This first statement shows that yes, printf DOES round */
   printf("%4.2f %4.2f\n",0.016,0.024);

/* 2 This one works ok */
   printf("%14.12f\n",2.0e-12);

/* 3 This is the curious statement */
   printf("%14.12f\n",1.0e-12);
}

produces the following result under Turbo C version 1.5: 

0.02 0.02
0.000000000002
0.000000000000

And more reasonable results under Turbo C version 1.0 and our
Unix machines here.

				Alan Myrvold
				ajmyrvold at violet.waterloo.edu