Overflow in mpz_cmp

[Marco Bodrato]

Ciao,
Il 2020-02-13 08:54 Guillaume Melquiond ha scritto:
> Note that mpz_cmpabs does not have any overflow issue, since absolute
> sizes are subtracted there. So, except maybe for homogeneity with
> mpz_cmp, it can keep using the optimized version.

I pushed a patch for both cmp and cmpabs. So that the second is ready 
for a change in the type of the field _mp_size for the mpz_t variables 
:-)

But you are right, the patch to cmpabs is not needed for the current 
code.

Il 2020-02-10 18:25 Guillaume Melquiond ha scritto:
> The bug was noticed when formally verifying this function.

Did you apply formal verification to other functions? Did they succeed?

Ĝis,
m