(* XXX preconditions: >= 0 *)
typedef int off_t