--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on January 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Fwd: Re: [Why3-club] frama-c/wp



[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