--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on November 2014 ---
[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 )