mbodin/coqr

A Coq formalisation of the R programming language

coqr's Issues

Bug with integer overflow with arithmetic operation

• R program that triggers the difference

> x <- 2147483647L ; x + 1L
> x <- 2147483647L ; x * x

• runR.native Output

[1] 2147483648
[1] 4611686014132420609

• R Output

[1] NA
Warning message:
In x + 1L : NAs produced by integer overflow

• Additional information

Haven't checked anything yet

Bug in arithmetic operation with NA as argument

• R program that triggers the difference

1 + NA

(Any sum using NA)

• runR.native Output

[1] NaN

• R Output

[1] NA 

• Additional information

I am wondering if it has something to do with using Double.add.
I noticed in bisect that this execution goes all the way from do_arith to R_binary. The checks at the source code (first, snd) return false (which seems ok). Then it jumps straight to calling R_binary.

In R_binary it skips the checks for array (makes sense) and in this check it enters. It ends up calling real_binary (source) and ends ups performing this operation (coqR code)