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

  • Subject: [Frama-c-discuss] Math functions in WP Plugin
  • From: frank at dordowsky.de (Frank Dordowsky)
  • Date: Fri, 6 Jun 2014 11:28:53 +0200 (CEST)
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?