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] Problem with real division

Hollas Boris (CR/AEY1) a ?crit :
> Do Jessie or Gappa also support an exact model for arithmetic in Q or R? This would be easier to handle for the engineer, but of course it couldn't detect overflow or underflow.

In fact, Gappa only works on real numbers; so, in a sense, Gappa only 
supports an exact model. (Floating-point operations are expressed as 
composition of exact real operations.)

Jessie works with several models, including exact arithmetic; it's just 
a matter of setting the argument of the JessieFloatModel pragma. Jessie 
will then interpret the floating-point operations according to the 
model. So Jessie and Gappa can also be used for exact arithmetic.

Note that, while working directly on real numbers, Gappa is designed to 
prove properties involving floating-point operations. So its results may 
be a bit disappointing when working on exact expressions, especially 
when compared to tools dedicated to real numbers.

> On the other hand, precision for real arithmetic varies in embedded systems. Many systems even use fixed point arithmetic. Thus, for embedded programming an adjustable precision would be useful.

Gappa supports floating-point and fixed-point arithmetic, in various 
precisions. Even exotic arithmetics can be encoded, and Gappa will prove 
things about them as long as they behave similarly to usual arithmetics. 
Jessie doesn't support (yet?) all of these arithmetics though, so it's 
not possible to use it to go from a C code to a Gappa file.

Best regards,

Guillaume