// Version 2: Better specification

#include <limits.h>

/*@ requires x > INT_MIN;
  @ ensures x >= 0 ==> \result == x;
  @ ensures x < 0 ==> \result == -x;
*/

int abs(int x) {
  if (x < 0)
	return -x;
  else
	return x;
}  

int main() {

abs(10);
abs(-20);
abs(INT_MIN);

}