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: https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2018-February/005401.html > 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 Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
