typedef /*@abstract@*/ int pivo;