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] Axiomatic Definition of Rounding Function

  • Subject: [Frama-c-discuss] Axiomatic Definition of Rounding Function
  • From: frank at dordowsky.de (Frank Dordowsky)
  • Date: Thu, 19 Jun 2014 09:19:12 +0200 (CEST)
I am trying to introduce the rounding function axiomatically but my 
definition seems not to be sufficient. Here is my example:

// file: round.h

/*@ axiomatic Rounding {
   @ logic integer lround(real x);
   @ axiom rounded_value:
   @    \forall real x ; -0.5  <= (x - lround(x)) < 0.5;
   @ }
   @*/

/*@ requires 0.0 <= x <= 1000.0;
   @ ensures \result == lround(x);
   @*/
int roundit(float x);

The implementation is as follows:

// file: round.c
#include "round.h"

int roundit(float x)
{
   return (int)(x+0.5);
}

When I try to prove this function with the float model (using
Alt-Ergo), I get the following error:

------------------------------------------------------------
--- Alt-Ergo (stderr) :
------------------------------------------------------------
File "/tmp/wp067b74.dir/typed_ref_int_float/roundit_assert_3_Alt-Ergo.mlw", line 183, characters 23-47:typing error: real and int cannot be unified

What is the reason for it, I have assumed that logic type integer is a
subset of logic type real?

When I replace the float model by the real model, there is no such
error, but Alt-Ergo is not able to prove the post condition. I am
probably overlooking something trivial, so thanks for your patience.

Frank