--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on December 2012 ---
Hello, I shall answer about Frama-C/WP, but not on Frama-C/Jessie ;-) With Oxygen : there is no direct support for PVS at all, unless via Why-2 With (future) Fluorine : Why2 output will not be maintained (and eventually removed). Why3 output will be fully supported, hence the related support for PVS. As far as a know, Why3 is now ready to address the next release of PVS, thanks to recent developments from Jean-Christophe. L.