--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on January 2015 ---
[forward to Frama-C list, since it is more related to Wp plugin than Why3, and it might be useful for other Frama-C users] Indeed, the syntax for the Why3 command line changed significantly since version 0.84. Until a new Frama-C/Wp is released, the small scripts provided by Khairul are probably good work-arounds. Beware anyway that there might be other use cases from Wp that might be needed to handle in those scripts (I mean, apart from handling specifically the options --list-provers and -I) - Claude -------- Forwarded Message -------- Subject: Re: [Why3-club] frama-c/wp Date: Tue, 13 Jan 2015 13:33:45 +0800 From: Khairul Azhar Kasmiran <kazarmy at gmail.com> To: why3-club at lists.gforge.inria.fr <why3-club at lists.gforge.inria.fr> Hello Junkil, What I've done is that I've renamed my? why3? binary to? why3-main and used the attached bash wrapper scripts as glue. You might need to change the paths accordingly. While I'm not a bash expert, I hope you find the scripts useful! Best regards, Dr. Khairul Azhar Kasmiran Room C3-14, Department of Computer Science, Faculty of Computer Science and Information Technology, Universiti Putra Malaysia, 43400 UPM Serdang, Selangor, Malaysia. Tel: +603 8947 1657 Fax: +603 8946 6576 On Tue, Jan 13, 2015 at 7:44 AM, Junkil (David) Park <juki14 at gmail.com <mailto:juki14 at gmail.com>> wrote: Hello, With the previous version of Why3, I could let frama-c/wp connect to Why3 (IDE and other provers) by (for example, ???> frama-c -wp -wp-prover why3ide test.c???). But, it seems that with the recent version of Why3, I am not able to do that. I think it is because Why3 commands has been recently change from ???why3ide??? to ???why3 ide???. If anyone can give an advice on this, I would appreciate it. Thanks, Junkil _______________________________________________ Why3-club mailing list Why3-club at lists.gforge.inria.fr <mailto:Why3-club at lists.gforge.inria.fr> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: why3 Type: application/octet-stream Taille: 140 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150113/1c727aa4/attachment-0002.obj> -------------- section suivante -------------- Une pi?ce jointe autre que texte a ?t? nettoy?e... Nom: why3ide Type: application/octet-stream Taille: 64 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150113/1c727aa4/attachment-0003.obj> -------------- section suivante -------------- _______________________________________________ Why3-club mailing list Why3-club at lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club