Sylvie Boldo

Gallery of proved programs

	⇑
⇐	Screenshot of gWhy (fully automatically proved)	⇒

KB3D, whatever hardware and compiler

This program was proved with previous versions of the tools (namely the Bore version of Frama-C and the 2.26 version of Why) and does not work anymore.

This is the same example as eps_line1 except that we are independent from the execution hardware and the compilation choices (extended registers, FMA).

#pragma JessieFloatModel(multirounding)
#pragma JessieIntegerModel(math)

//@ logic integer l_sign(real x) = (x >= 0.0) ? 1 : -1;

/*@ requires e1<= x-\exact(x) <= e2;   
  @ ensures  (\result != 0 ==> \result == l_sign(\exact(x))) &&
  @          \abs(\result) <= 1 ;
  @*/
int sign(double x, double e1, double e2) {
  
  if (x > e2)
    return 1;
  if (x < e1)
    return -1;
  return 0;
}
 
/*@ requires 
  @   sx == \exact(sx)  && sy == \exact(sy) &&
  @   vx == \exact(vx)  && vy == \exact(vy) &&
  @   \abs(sx) <= 100.0 && \abs(sy) <= 100.0 && 
  @   \abs(vx) <= 1.0   && \abs(vy) <= 1.0; 
  @ ensures
  @    \result != 0 
  @      ==> \result == l_sign(\exact(sx)*\exact(vx)+\exact(sy)*\exact(vy))
  @            * l_sign(\exact(sx)*\exact(vy)-\exact(sy)*\exact(vx));
  @*/

int eps_line(double sx, double sy,double vx, double vy){
  int s1,s2;

  s1=sign(sx*vx+sy*vy, -0x1.90641p-45, 0x1.90641p-45);
  s2=sign(sx*vy-sy*vx, -0x1.90641p-45, 0x1.90641p-45);
 
  return s1*s2;
}