--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on August 2009 ---
Hello Guillaume, 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. 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. Best regards, Boris #pragma JessieFloatModel(strict) /*@ requires 0x1p-1000 <= R1 <= 0x1p1000 && 0x1p-1000 <= R2 <= 0x1p1000; ensures \result > 0; */ double R_ges(double R1, double R2) { return 1.0/( 1.0/R1 + 1.0/R2 ); } int main(void) { double R; R = R_ges(100, 200); return 0; }