# 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

*Subject*: [Frama-c-discuss] WP drivers and Why3*From*: loic.correnson at cea.fr (Loïc Correnson)*Date*: Tue, 31 Oct 2017 09:53:03 +0100*In-reply-to*: <2DBC6AF1-937E-4EF1-9913-5CA71D94632B@udel.edu>*References*: <91A536F5-5561-450F-8DFD-13CD935C276D@udel.edu> <F721A86F-2A72-4B35-BDED-2EFA372E13B1@cea.fr> <2DBC6AF1-937E-4EF1-9913-5CA71D94632B@udel.edu>

> 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? No you probably donâ€™t have to. ACSL operators on sets are already bound to these theories ; actually, this is the reason why we provide these theories with WP. And you can also bind your own symbols on them, too. However, if you face some problem do not hesitate to report on. Here is a typical exemple of how to use drivers. File abs.c : /*@ axiomatic Absolute { logic integer ABS(integer x) ; } */ /*@ ensures \result == ABS(x) ; */ int abs(int x) { if (x < 0) return -x ; return x ; } Now you want to provide a theory for logic function ABS (here in Why3, but you can do the same for Alt-Ergo and Coq). In the theory, you may use the same name or a different one than in ACSL: File abs.why : theory Abs use import int.Int function my_abs int : int axiom abs_pos : forall x:int. x>=0 -> my_abs x = x axiom abs_neg : forall x:int. x<=0 -> my_abs x = -x end The driver for WP is the following abs.driver file: library "abs": why3.file := "abs.why"; logic integer ABS (integer) = "my_abs" ; All together: $ frama-c -wp -wp-prover cvc4 -wp-driver abs.driver abs.c [kernel] Parsing abs.i (no preprocessing) [wp] warning: Missing RTE guards [wp] 1 goal scheduled [wp] Proved goals: 1 / 1 Qed: 0 (4ms) cvc4: 1 (50ms) The generated goal for Why3 is: (* ---------------------------------------------------------- *) (* --- Post-condition (file abs.i, line 13) in 'abs' --- *) (* ---------------------------------------------------------- *) theory VCabs_post use import bool.Bool use import int.Int use import int.ComputerDivision use import real.RealInfix use import Qed.Qed use import int.Abs as IAbs use import map.Map use import Cint.Cint use import abs.Abs goal WP "expl:Post-condition (file abs.i, line 13) in 'abs'": forall i_1 i : int. ((is_sint32 i)) -> ((is_sint32 i_1)) -> (if (i < 0) then ((i + i_1) = 0) else (i_1 = i)) -> (((my_abs i)) = i_1) end Consult file `frama-c -print-share-path`/wp/wp.driver for many other binding examples. L. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20171031/0b1ab89d/attachment-0001.html>

**References**:**[Frama-c-discuss] Define a Logic function returning an array***From:*wuwenhao at udel.edu (Wenhao Wu)

**[Frama-c-discuss] Define a Logic function returning an array***From:*loic.correnson at cea.fr (Loïc Correnson)

**[Frama-c-discuss] WP drivers and Why3***From:*siegel at udel.edu (Stephen Siegel)

- Prev by Date:
**[Frama-c-discuss] WP drivers and Why3** - Next by Date:
**[Frama-c-discuss] Does WP support declare ghost variables of logic types ?** - Previous by thread:
**[Frama-c-discuss] WP drivers and Why3** - Next by thread:
**[Frama-c-discuss] Define a Logic function returning an array** - Index(es):