--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on November 2011 ---
Le 04/11/2011 09:55, Boris Hollas a ?crit : > On Thu, 2011-11-03 at 13:11 +0100, Claude Marche wrote: >> From your message, I guess you mean that you are using the Why3 >> backend (since Vampire is not available in Why 2.30) > yes, I had that problem with why3. However, Vampire also works with the > why2-gui. > You're right, my mistake. >> First of all, you may want to check that your proofs still work with >> the former Why 2.30 back-end, using frama-c -jessie -jessie-atp=gui > indeed, with the why2 back-end, the code verifies as before. Good! Then now, using why3ide, and "split" button, is everything proved or not? If not, could you send more details? source code? - Claude