+/*
+ * Takes an abstract value having sign `sign_z', exponent `exp_z', and significand
+ * `sig_z' and returns the appropriate value corresponding to the abstract input.
+ *
+ * The abstract value is simply rounded and packed into the format. If the abstract
+ * input cannot be represented exactly an inexact exception is raised. If the
+ * abstract input is too large, the overflow and inexact exceptions are both raised
+ * and an infinity or maximal finite value is returned. If the abstract value is
+ * too small, the value is rounded to a subnormal and the underflow and inexact
+ * exceptions are only raised if the value cannot be represented exactly with
+ * a subnormal.
+ *
+ * The input significand `sig_z' has it's binary point between bits 30 and 29,
+ * this is seven bits to the left of its usual location. The shifted significand
+ * must be normalized or smaller than this. If it's not normalized then the exponent
+ * `exp_z' must be zero; in that case, the result returned is a subnormal number
+ * and is must not require rounding. In the more usual case where the significand
+ * is normalized, the exponent must be one less than the *true* exponent.
+ *
+ * The handling of underflow and overflow is otherwise in alignment with IEC/IEEE.
+ */