Here's a challenge for floating point lovers.

[Ray Butterworth]

Ever tried to come up with a manifest for a specific floating point value?
It is next to impossible.

For instance, using knowledge of what the bits look like,
#define MAXFLOAT  (*(double*)"\377\177\377\377\377\377\377\377")
works on vaxes, but it makes really disgusting assumptions about the
alignment of string constants and doubles.

But, if we assign that value to a variable, print out the result,
and then enter that result into a header file, when it gets
processed again the value is wrong.  For instance:

Stock "cc" command gives:
                      true max  ff7fffffffffffff  1.70141183460469229000e+38
       1.70141183460469229e+38  ff7ffffffffffdff  1.70141183460469225000e+38
   4096*4.15383748682786209e34  ff7ffffffffffeff  1.70141183460469227000e+38

"gcc" command gives:
                      true max  ff7fffffffffffff  1.70141183460469229000e+38
       1.70141183460469229e+38  ff7ffffffffffeff  1.70141183460469227000e+38
   4096*4.15383748682786209e34  ff7fffffffffffff  1.70141183460469229000e+38

So, simply using the output value is wrong on GCC and twice as bad on CC.
Using "4096*4.15383748682786209e34" works with GCC, but not with CC.
In fact, I haven't found a constant that will work with CC other than
the kludgy mess with the (double*), which will cause hardware faults
on many (non-vax) machines.

Anyone know how to solve this problem in general,
or even in this specific case?

Does ANSI X3.159 require the ability to define such a constant?

Here's the program that produced the above:

#include <stdio.h>

#define MAXFLOAT  (*(double*)"\377\177\377\377\377\377\377\377")

	static void
test(label, value)
	char *label;
	double value;
{
	auto int index;

	printf("%30s  ", label);
	for (index=0; index<sizeof(value); ++index)
		printf("%2.2x", index[(unsigned char*)&value]);
	printf("  %25.20e\n", value);
}



main() {
	auto double max = MAXFLOAT;

	test("true max", max);
	test("1.70141183460469229e+38", 1.70141183460469229e+38);
	test("4096*4.15383748682786209e34", 4096*4.15383748682786209e34);
}