/* Work around precision issue in Frama-C Oxygen regarding % */
/*@ requires y != 0;
    assigns \result \from x,y;
    ensures -(y) < \result < y || y<\result< -y;
    ensures \result == x%y;
*/
int mod(int x, int y);

int pgcd(int x, int y) {
     int a = x, b = y;
     while(b!=0) {
          int tmp = mod(a,b);
          a = b; b = tmp;
     }
     return a;
}

int P;

void test() {
     P=pgcd(121,77);
}

int ppcm(int x, int y) {
     int a = x, b = y;
     while(b!=0) {
          int tmp = mod(a,b);
          a = b; b = tmp;
     }
     return x * y / a;
}

void test2() {
     P=ppcm(49,28);
}

/*@ requires a<=b;
  ensures a<=\result<=b;
*/
int interval(int a, int b);