# 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

**Follow-Ups**:**[Frama-c-discuss] Axiomatic Definition of Rounding Function***From:*mohamed.iguernelala at ocamlpro.com (Mohamed Iguernelala)

**[Frama-c-discuss] Axiomatic Definition of Rounding Function***From:*pascal.cuoq at gmail.com (Pascal Cuoq)

- Prev by Date:
**[Frama-c-discuss] Using frama-c script to get proof obligations** - Next by Date:
**[Frama-c-discuss] Axiomatic Definition of Rounding Function** - Previous by thread:
**[Frama-c-discuss] Using frama-c script to get proof obligations** - Next by thread:
**[Frama-c-discuss] Axiomatic Definition of Rounding Function** - Index(es):