ASSUME
ASSUME(width > 0);
ASSUME(height > 0);
ASSUME(0 <= dstbitoffs && dstbitoffs < 32);
ASSUME(width > 0);
ASSUME(height > 0);
ASSUME(planecount > 0);
ASSUME(planecount == 1 ||