After a recent upgrade of why3 using OPAM I am getting a lot of warnings every
time I invoke a prover through frama-c as well as a message about ambiguous
path. While I thought I had removed everything left behind from previous
incarnations of Why3, I can’t rule out something
Got left behind
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:
>
> bot
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.
