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] why3 1.1.0 support in frama-c/wp

  • Subject: [Frama-c-discuss] why3 1.1.0 support in frama-c/wp
  • From: loic.correnson at cea.fr (Loïc Correnson)
  • Date: Thu, 10 Jan 2019 11:13:13 +0100
  • In-reply-to: <CAP6v9C7CgOsShQap7BNX2W4u34vyiEQiP=4XrHw2UiM0Su_VWA@mail.gmail.com>
  • References: <CAP6v9C7CgOsShQap7BNX2W4u34vyiEQiP=4XrHw2UiM0Su_VWA@mail.gmail.com>
Hi Benjamin,

Thanks a lot for your experience report and for sharing your repo.

Actually, making WP resources and the generated proof obligations in sync with Why-3 and Coq is a recurrent challenge. On Frama-C developper’s side, we have routines to automatically produce them thanks to custom  Why-3 drivers, but the process is a bit hacky and still require manual process and manual Coq proof migrations.

So solve these issues, and also the issues related to warnings, we plan to make Why-3 API a direct dependency of the WP plug-in, and to no longer provide the native output for Coq and Alt-Ergo. This is a major refactoring that will be probably available in 2019 but we can not promise it.

We also plan to make Why-3 theories directly accessible from ACSL in order to make the two platforms closer to each others. But this feature still requires some experiments and discussions with ACSL board.

In the meanwhile, the next release of Frama-C will be in sync with the most recent Why-3 1.x and Coq 8.x

The development of Frama-C is not hosted in GitHub, although pull requests are very welcomed !
We would try our best for integrating relevant proposals. I definitely will have a look at your repo.

Best regards,
	Loïc.

> Le 13 déc. 2018 à 19:25, Benjamin Nauck <benjamin at nauck.se> a écrit :
> 
> Hi,
> 
> When I was installing frama-c I noticed that it lacked support for why3 >= 1.0.0. Not really a big deal, but I thought it would be a fun project to try to get it working (both to learn how frama-c works under the hood and to tinker with some ml). I'm not sure if anyone has done this already, if so I failed find it :)
> 
> Anyway, I now have a version of frama-c/wp which can use why3 1.1.0 instead of 0.xx (changes should work with 1.0.0 too). I've tested it with alt-ergo (2.2.0), cvc4 (1.6), z3 (4.8.3), gappa (1.3.2), and (coq 8.8.2) by throwing "isqrt.c" at it (from Tomas Härdin blog post from november). I should mention that coq wasn't able to prove anything, but that's also the the result I get with the old version.
> 
> It needs some more testing and I need to figure out what to do with all the "axiom X does not contain any local abstract symbol" warnings that I get, but it's getting there!
> 
> Regarding the warning:
> File "/Users/hyarion/.opam/test3/share/frama-c/wp/why3/Qed.why", line 64, characters 6-17:
> warning: axiom c_euclidian does not contain any local abstract symbol (contains: int, (=), (+), ( * ), div, mod)
> I think I read somewhere that changing those axioms to lemmas fixes the issue, and it does, but I'm not quite sure if that's the preferred solution or if it could have some side effects. Would it be safe to solve it like this or do you have any other suggestions?
> 
> It would be nice to throw some more tests at it to verify compatibility. Are there any unit tests (or similar) for wp so I can make sure everything works as intended?
> 
> By the way, I noticed that the github repository is some kind of snapshot mirror, which makes me wonder: is the main repository available somewhere else?
> And what's the preferred way to contribute to the project? open pull requests on github? send in patches via the issue tracker? or by mailing them to this list?
> 
> The repo is located here if anyone is curious:
> https://github.com/hyarion/Frama-C/tree/wp-why3-1.x.x <https://github.com/hyarion/Frama-C/tree/wp-why3-1.x.x>
> 
> And if you want to try it out, then it's just one opam command away:
> opam pin frama-c https://github.com/hyarion/Frama-C.git#wp-why3-1.x.x <https://github.com/hyarion/Frama-C.git#wp-why3-1.x.x>
> 
> 
> // Benjamin Nauck
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190110/05d7b01f/attachment-0001.html>