--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on June 2014 ---
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