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 8:11 AM, Claude March? <Claude.Marche at inria.fr> wrote:
>
> Probably the same problem as
> http://lists.gforge.inria.fr/pipermail/why-discuss/2014-October/000697.html
>
> You should run fram-c with extra option: -cpp-extra-args="-I$(frama-c
> -print-share-path)/libc"

Indeed, that fixes the ranges; and leaves me in the same place I got
by manually search and replacing the ranges.

Still at 17 out of 58 failing for that trivial one statement example,
but this might now be more alt-ergo's fault.

It's mostly failing on the ones that contain many to_uint64s ...
though I'm not quite sure why the -wp-rte is emitting those, if each
operation is checked to not overflow, then wrapping a subexpression
with a to_int64 should not do anything.