Title
Bad postcondition for set_default_resource
Status
c++20
Section
[mem.res.global]
Submitter
Casey Carter

Created on 2017-05-09.00:00:00 last changed 45 months ago

Messages

Date: 2017-06-15.19:55:58

Proposed resolution:

This wording is relative to N4659.

  1. Modify [mem.res.global] as follows:

    memory_resource* set_default_resource(memory_resource* r) noexcept;
    

    -4- Effects: If r is non-null, sets the value of the default memory resource pointer to r, otherwise sets the default memory resource pointer to new_delete_resource().

    -5- Postconditions: get_default_resource() == r.

    -6- Returns: The previous value of the default memory resource pointer.

    -7- Remarks: […]

Date: 2017-06-15.00:00:00

[ 2017-06-15, Moved to Tentatively Ready after 6 positive votes on c++std-lib ]

Date: 2017-06-15.00:00:00

[ 2017-06-13, Casey Carter revises proposed wording ]

I suggest to strike the Postconditions paragraph ([mem.res.global]/5) completely, as in LWG 2522

Date: 2017-05-15.00:00:00

[ 2017-05-13, Tim comments ]

This is the same issue as LWG 2522, which just missed the Fundamentals TS working draft used for the merge. A similar resolution (simply striking the Postconditions: paragraph) might be better.

Previous resolution [SUPERSEDED]:

This wording is relative to N4659.

  1. Modify [mem.res.global] as follows:

    memory_resource* set_default_resource(memory_resource* r) noexcept;
    

    -4- Effects: If r is non-null, sets the value of the default memory resource pointer to r, otherwise sets the default memory resource pointer to new_delete_resource().

    -5- Postconditions: If r is non-null, get_default_resource() == r. Otherwise, get_default_resource() == new_delete_resource().

    -6- Returns: The previous value of the default memory resource pointer.

    -7- Remarks: […]

Date: 2017-05-09.00:00:00

The specification of set_default_resource in N4659 [mem.res.global] reads:

memory_resource* set_default_resource(memory_resource* r) noexcept;

-4- Effects: If r is non-null, sets the value of the default memory resource pointer to r, otherwise sets the default memory resource pointer to new_delete_resource().

-5- Postconditions: get_default_resource() == r.

-6- Returns: The previous value of the default memory resource pointer.

-7- Remarks: […]

It is apparent that the effects specified in para 4 cannot — and indeed should not — achieve the postcondition specified in para 5 when r is null.

History
Date User Action Args
2021-02-25 10:48:01adminsetstatus: wp -> c++20
2017-07-30 20:18:47adminsetstatus: voting -> wp
2017-06-26 13:46:20adminsetstatus: ready -> voting
2017-06-15 19:55:58adminsetmessages: + msg9268
2017-06-15 19:55:58adminsetstatus: new -> ready
2017-06-13 19:03:18adminsetmessages: + msg9252
2017-05-13 18:22:50adminsetmessages: + msg9184
2017-05-13 10:18:06adminsetmessages: + msg9178
2017-05-09 00:00:00admincreate