--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on October 2017 ---
[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