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] Math functions in WP Plugin

Hi,
Yes, those functions are not defined in WP.
However, you can extend WP with your own specifications for these symbols by using ?drivers?.
See WP manual ? 2.3.10.

For instance, you may define this simple driver:
# cat exp. driver
altergo.file += "exp.mlw" ;
coq.file += "exp.v" ;
logic real \exp(real) = "exp" ;

You should put axioms and definitions for the ? exp ? function for alt-ergo, coq or Why-3 in appropriate files, as suggested above.

Then, you load this driver within WP:
# frama-c -wp -wp-driver exp.driver ?

and the generated proof obligations will be linked with the resources files listed in the driver.

	L.

PS : this mechanism is not restricted to ACSL builtins, it is applicable to user-defined symbols and predicates.



Le 6 juin 2014 ? 11:28, Frank Dordowsky <frank at dordowsky.de> a ?crit :

> I am trying to define logical functions using the mathematical functions \exp and \floor. The syntactic checks are fine, but when trying to prove my code with the WP plugin I get the following error messages:
> 
> [wp] user error: Builtin \floor(real) not defined
> [wp] user error: Builtin \exp(real) not defined
> [wp] failure: Logic '\exp' undefined
> 
> I have checked the document ACSL Version 1.7 - Implemetation in Fluorine-20130601, but there is no hint that these functions are not available. I could not find any information in the WP manual and man pages. I am using Frama-C Fluorine-20130601 and WP 0.7. What math functions are recognized by WP? Or is there anything I must do additionally?
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss