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

Hello,

(Currently) Alt-Ergo does not consider that "int" is a subtype of 
"real". This is why it says "typing error: real and int cannot be 
unified ". This should evolve with our new (experimental) input language 
based on SMT2.

A workaround would be to introduce an explicit cast between int and real.

- Mohamed.

-- 
Senior R&D Engineer, OCamlPro
Research Associate, VALS team, LRI.
http://www.iguer.info

Le 19/06/2014 09:19, Frank Dordowsky a ?crit :
>
> 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
> _______________________________________________
> 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