--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on March 2018 ---
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>