--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on March 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] (no subject)



Lois

I'm using

Why3 platform, version 0.88.3


also installed via OPAM

On Fri, Mar 23, 2018 at 11:32 AM, Loïc Correnson <loic.correnson at cea.fr>
wrote:

> Hi Alwyn,
>
> > [Config] reading extra configuration file /Users/agoodloe/.opam/4.04.2/
> share/frama-c/wp/why3/why3.conf
> > File "/Users/agoodloe/.opam/4.04.2/share/frama-c/wp/why3/Qed.why", line
> 68, characters 6-17:
> > warning: axiom c_euclidian does not contain any local abstract symbol
>
> Those warning are produced by Why-3 when we are defining some axioms on
> regular symbols.
> There are also some other warnings when using polymorphic constants, such
> as ACSL « \nil » constructor for lists.
> All those Why-3 warning are normal, and we will work to silence them in
> (some) future version of Frama-C.
> You shall ignore them.
>
> > but it also produces
> >
> > Ambiguous path:
> > both /Users/agoodloe/.opam/4.04.2/share/why3/modules/Matrix.mlw
> > and /var/folders/9d/hlf0_5_17993l6xr42bjdfrm0cwq24/T/
> wp04a2c9.dir/typed/Matrix.why
>
> The `Matrix` theory is generated by WP for modelling C-arrays. However, I
> did not see this warning for a long time now, although I remember it.
> Or, more probably, I forget it with all the other ones. Just to be sure,
> which version of Why-3 are you using ?
>
>         L.
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss




-- 
Alwyn E. Goodloe, Ph.D.
agoodloe at gmail.com

Research Computer Engineer
NASA Langley Research Center
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180323/79b065b2/attachment.html>