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: benjamin at nauck.se (Benjamin Nauck)
  • Date: Thu, 13 Dec 2018 19:25:15 +0100
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

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


// Benjamin Nauck
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20181213/0823e0c7/attachment.html>