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

> 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>