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
