B.1.11 Get_Status_Output Procedure

The main documentation of the Get_Status_Output Procedure contains additional explanation of this code listing.

  subroutine Get_Status_Output (Status_String, S)

    ! Input variable.

    type(Status_type), intent(in) :: S  ! Status.

    ! Output variable.

    ! Output string for this Status.
    type(character,*), intent(out) :: Status_String   


    ! Verify requirements.

    VERIFY(Valid_State(S),1)   ! S is valid.

    ! Determine which output string is to be set.

    Status_String = status_flag(S%status)%output_string

    ! Verify guarantees.

    ! Status_String should be what it was set to.
    VERIFY(Status_String == status_flag(S%status)%output_string,2)

  end subroutine Get_Status_Output

Michael L. Hall