Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP failing to prove a simple absence of RTE unsigned overflow

On Tue, Nov 4, 2014 at 7:04 AM, Mohamed Iguernelala
<mohamed.iguernelala at ocamlpro.com> wrote:
> Hi,
>
> I looked into one of the unproved VCs
> ("secp256k1_fe_mul_inner_assert_rte_unsigned_overflow_38" attached),
> and I think that it is not valid.
>
> The VC is of the form:
>
> goal overflow_38:
>   "some context" ->
>   x_9 <= 67108863 ->
>   x_10 <= 1073741823 ->
>   x_9 * x_10 <= 4294967295
>
> So, you are trying to show that "x_9 * x_10 <= 4294967295" always holds
> under the given context  (i.e. for every
> possible values for x_9 and x_10). But this is not true when taking, for
> instance, x_9 = 67108863  and x_10 = 1073741823.

Indeed, but that means the RTE generated assertions are incorrect:
All the operations in the code are uint64_t, so the overflow target
should have been against 2^64-1, not 2^32-1.

I should have noticed this before, it's even clear in the frama-c gui.

Manually fixing the the range being checked to 2^64-1, and changing
the to_uint32's to to_uint64s where they are 64 bit intermediates in
the C makes more of the proofs pass but not all of them. (e.g. not
secp256k1_fe_mul_inner_assert_rte_unsigned_overflow_2 )