Thanks Claude, You are correct the OSX temp directory as specified in the environment variable TMPDIR appears to be used. Neither the path nor the environment variable are in the .why3.conf directory. If why3 isn't directing this use, then it might be wp telling it to use this directory.
-- Alwyn E. Goodloe Ph.D. a.good...@nasa.gov Research Computer Engineer NASA Langley Research Center On 3/12/18, 3:39 AM, "Why3-club on behalf of Claude Marché" <why3-club-boun...@lists.gforge.inria.fr on behalf of claude.mar...@inria.fr> wrote: 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 _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club