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] How to set WP and Why provers

  • Subject: [Frama-c-discuss] How to set WP and Why provers
  • From: kenji_fujitani at jtekt.co.jp (Kenji Fujitani)
  • Date: Thu, 17 Sep 2020 06:00:12 +0000
Dears,

I have try set up framna-c's Plugins, and their provers again and again,….

But I couldn’t make sure its mechanism and method of set up process is OK or not.

Please teach me What is going on, and show me correct set up process.



The set up process is like bellow.

1) Install opam

   $sudo add-apt-repository ppa:avsm/ppa

   $sudo apt update

   $sudo apt install opam

   $opam init

   $eval ‘opam config env’

   Opam Version =2.0.4



3)Setup Why3 Version1.3.3

  $sudo apt-get install libgmp-dev libgtksourceview2.0-dev m4

   $opam install why3 why3-ide alt-ergo

[cid:image001.png at 01D68D03.39908840]   $why3 config --full-config( or --list-provers)

[I can’t know what is occurred.]     ==>Sometimes Error is occurred as bellow

          Alt-Ergo2.3.3 is mismatch on your environment.

          Older version is 2.2.1 or ,.....

     Then try to downgrade alt-ergo to 2.2.0(for example)

   $why3 config --fiull-config

     ====> if passed, go to next step



４）$opam install depext

    $opam depext frama-c

    $opam install frama-c(Set Version; like frama-c.16.0)



=>Fortunately, Frama-c is available, but I have some doubt whether its prover version fit to environment or not.



5) I’ve try to research WP plugin’s mechanism by bellow.

  Example:swap function

  $frama-c -wp-prover /home/username/.why3.conf

  $frama-c -wp -wp-rte swap.c



  Then Error is occurred.

  [kernel] Parsing swap.c(with preprocessing)

  [rte]annotating Function swap

[cid:image001.png at 01D68D03.39908840]  [wp]4 goals scheduled

[Alt-Ergo Version is mismatch?  Or Frama-C Version’s mismatch?]  [wp][Alt-Ergo 2.2.0]Goal typed_swap_assert_rte_access_4:Timeout (Qed:2ms)(10s)

  [wp][Alt-Ergo 2.2.0]Goal typed_swap_assert_rte_access_3:Timeout (Qed:1ms)(10s)

[wp][Alt-Ergo 2.2.0]Goal typed_swap_assert_rte_access_:Timeout (Qed:1ms)(10s)

  [wp][Alt-Ergo 2.2.0]Goal typed_swap_assert_rte_access_2:Timeout (Qed:2ms)(10s)

  [wp]Proved goals: 0/4

  Alt-Ergo 2.2.0:  0 (interrupted: 4)



  Why Alt-Ergo does not proceed?



  Sincerely, yours

  Ken

*******************************************************************************

株式会社ジェイテクト

先行システム開発部　第一開発室　SR-G

藤谷　賢治



〒444-2106　

愛知県岡崎市真福寺町字深山1番地10

株式会社ジェイテクト　花園工場　

TEL:0564-27-3420

*******************************************************************************



JTEKT prepared a Global Privacy Policy for EU residents.
Please visit the website.　https://www.jtekt.co.jp/e/privacy3.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200917/df6e0c26/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image001.png
Type: image/png
Size: 396 bytes
Desc: image001.png
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200917/df6e0c26/attachment-0003.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image002.emz
Type: application/octet-stream
Size: 1094 bytes
Desc: image002.emz
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200917/df6e0c26/attachment-0002.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image005.png
Type: image/png
Size: 1375 bytes
Desc: image005.png
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200917/df6e0c26/attachment-0004.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image006.emz
Type: application/octet-stream
Size: 1425 bytes
Desc: image006.emz
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200917/df6e0c26/attachment-0003.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: image007.png
Type: image/png
Size: 1801 bytes
Desc: image007.png
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200917/df6e0c26/attachment-0005.png>