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