[Gawk] Bug in arithmetic comparisons

[Seb]

Hello,

I think there is a bug in the comparisons that gawk (3.1.8) makes in numeric
context. Here is an example of what I get :

$ echo "12.10 12.10" | awk 'BEGIN{print ($1 == $2) ? 1 : 0}'
  1
$ echo "12.10 12.1" | awk 'BEGIN{print ($1 == $2) ? 1 : 0}'
  1
$ echo "12.10 12.1" | awk 'BEGIN{print ($1 == $2+0) ? 1 : 0}'
  0

I don't know why, but in the third example, the addition seems to change the 
type
of "12.1" from strnum into string, so that the comparison is a string comparison
and is hence false.

The manual (section 5.10.1) specifies that strnum is the type of input strings
that can be taken as numeric (verified in the second example) and that once a
type is attributed, it can't be changed. So I think it's a bug somewhere (even 
if
I misunderstood the manual, I think "$2+0" should accordingly to POSIX be of
numeric type, so that the comparison is strnum vs. numeric, which is resolved in
a numeric context). Am I wrong ? :)


Take care,
Seb.