Le 09/03/2018 à 21:42, Goodloe, Alwyn E. (LARC-D320) a écrit :
> warning: axiom c_euclidian does not contain any local abstract symbol

The Frama-C developer team is aware of this issue:


> Ambiguous path:
> both /Users/agoodloe/.opam/4.04.2/share/why3/modules/Matrix.mlw
> and
> /var/folders/9d/hlf0_5_17993l6xr42bjdfrm0cwq24/T/wp10b1ad.dir/typed/Matrix.why

This second path has a strange shape, seems more like a temporary path
for me.

I suggest that you edit your .why3.conf file and search for the
"loadpath" items in the [main] section.

If the path above appear there, then remove it.

Alternatively, if you're not afraid of losing specific settings of your
Why3 config, then just remove .why3.conf and rerun

why3 config --detect

- Claude

Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - Île-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |
Why3-club mailing list

Reply via email to