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