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

[Frama-c-discuss] (no subject)



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.