--- layout: fc_discuss_archives title: Message 8 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 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.