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] WP drivers and Why3

I’m interested in the drivers but am a little unclear on the details of how to make them work.
Why3 has some theories in its “theories” directory.  I’m interested in the ones in the file set.why, in particular, Fset and Fsetint.    I’d like to be able to use the predicates and functions defined there in my ACSL contracts (and have those translated appropriately when I use Frama-C+WP+Why3).  

Should I create a WP driver file corresponding to those theories?    Can you show a sample of what goes in the driver file or any other details?    Also, is there an issue with conflicts with the existing ACSL set operations?

Thanks,
Steve


> On Oct 27, 2017, at 3:47 AM, Loïc Correnson <loic.correnson at cea.fr> wrote:
> 
> Hi,
> 
>> Is it possible to express a logic function returning an array in ACSL?
> 
> No it is not possible, unfortunately. The ACSL-By-Example document illustrate how to write logic predicates in ACSL dealing with C-arrays, but without manipulating « logic » arrays directly.
> Moreover, let me recall that SMS solvers usually deals with infinite arrays, which is probably not what you want to deal with. So you might need to design a theory of finite arrays first.
> 
> From WP point of view, you can declare an abstract datatype and logic functions that manipulate such a type, and provide separately a proper implementation of these symbols in Why-3 / Alt-Ergo / Coq.
> Then you can bind ACSL logic symbols to Why-3 / Alt-Ergo / Coq ones by using WP drivers. See the WP manual § 2.4.10, p. 36 for details.
> A typical exemple of driver is provided by WP itself, to bind predefined ACSL symbols (or memory model functions). You may have a look at it:
> 
> $ less `frama-c -print-share-path`/wp/wp.driver
> 
> Using drivers, you can also put structural properties on drivers (associativity and such) which allow for early simplifications in Qed.
> 	L.
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss