Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Fwd: Re: [Why3-club] frama-c/wp
  • From: Claude.Marche at inria.fr (Claude Marche)
  • Date: Tue, 13 Jan 2015 07:40:13 +0100
  • In-reply-to: <CA+Tazt4pnu811TkPtsciiqBKcekBU4N75U==wdAdEbmLoObvWw@mail.gmail.com>
  • References: <CA+Tazt4pnu811TkPtsciiqBKcekBU4N75U==wdAdEbmLoObvWw@mail.gmail.com>
[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