--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on June 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Math functions in WP Plugin



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?