/*@
 requires \valid(i);
 requires \valid(j);
 requires \valid(r);
 assigns *r;
 behavior normal:
	assumes r;
	assigns *r;
	ensures *j <= \at(*r,Here) && *i <= \at(*r,Here);
	ensures \at(*r,Here) == *j || \at(*r,Here) == *i ;
	ensures \result == 0;
 behavior r_null:
	assumes !r;
	assigns \nothing;
	ensures \result == -1;
*/
int max(int *r, int* i, int* j) { 
  if (!r) return -1; 
  *r = (*i < *j) ? *j : *i; 
  return 0; 
}