Skip to content

[unique.ptr.single] Align preconditions and postconditions with the guidelines #7982

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

[unique.ptr.single] Align preconditions and postconditions with the guidelines #7982

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
118e784
[unique.ptr.single] Align preconditions and postconditions with the g…
MikailBag Jun 22, 2025
1f2cbc2
Another set of changes
MikailBag Jun 22, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions source/memory.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2330,7 +2330,7 @@

\pnum
\ensures
\tcode{get() == nullptr}. \tcode{get_deleter()}
\tcode{get() == nullptr} is \tcode{true}. \tcode{get_deleter()}
returns a reference to the stored deleter.
\end{itemdescr}

Expand Down Expand Up @@ -2358,7 +2358,7 @@

\pnum
\ensures
\tcode{get() == p}. \tcode{get_deleter()}
\tcode{get() == p} is \tcode{true}. \tcode{get_deleter()}
returns a reference to the stored deleter.
\end{itemdescr}

Expand Down Expand Up @@ -2390,7 +2390,7 @@

\pnum
\ensures
\tcode{get() == p}.
\tcode{get() == p} is \tcode{true}.
\tcode{get_deleter()} returns a reference to the stored
deleter. If \tcode{D} is a reference type then \tcode{get_deleter()}
returns a reference to the lvalue \tcode{d}.
Expand Down Expand Up @@ -2446,7 +2446,7 @@
\pnum
\ensures
\tcode{get()} yields the value \tcode{u.get()}
yielded before the construction. \tcode{u.get() == nullptr}.
yielded before the construction. \tcode{u.get() == nullptr} is \tcode{true}.
\tcode{get_deleter()} returns a reference
to the stored deleter that was constructed from
\tcode{u.get_deleter()}. If \tcode{D} is a reference type then
Expand Down Expand Up @@ -2492,7 +2492,7 @@
\pnum
\ensures
\tcode{get()} yields the value \tcode{u.get()}
yielded before the construction. \tcode{u.get() == nullptr}.
yielded before the construction. \tcode{u.get() == nullptr} is \tcode{true}.
\tcode{get_deleter()} returns a reference
to the stored deleter that was constructed from
\tcode{u.get_deleter()}.
Expand Down Expand Up @@ -2549,8 +2549,8 @@

\pnum
\ensures
If \tcode{this != addressof(u)},
\tcode{u.get() == nullptr},
If \tcode{this != addressof(u)} is \tcode{true},
Copy link
Author

@MikailBag MikailBag Jun 22, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps this (and similar condition below) should be inverted to \tcode{this == addressof(u)} is \tcode{false}.
I'm not sure which way is more readable

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wonder whether we can simply say "this == addressof(u) || u.get() == nullptr is true".

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But there is also an else branch, so it will look like this:

* `this == addressof(u) || u.get() == nullptr` is `true`
* `this != addressof(u)` is `true` or `u.get()` is unchanged

Looks a bit too complex to me.

\tcode{u.get() == nullptr} is \tcode{true},
otherwise \tcode{u.get()} is unchanged.

\pnum
Expand Down Expand Up @@ -2588,7 +2588,7 @@

\pnum
\ensures
\tcode{u.get() == nullptr}.
\tcode{u.get() == nullptr} is \tcode{true}.

\pnum
\returns
Expand All @@ -2607,7 +2607,7 @@

\pnum
\ensures
\tcode{get() == nullptr}.
\tcode{get() == nullptr} is \tcode{true}.

\pnum
\returns
Expand Down Expand Up @@ -2644,7 +2644,7 @@
\begin{itemdescr}
\pnum
\expects
\tcode{get() != nullptr}.
\tcode{get() != nullptr} is \tcode{true}.

\pnum
\returns
Expand Down Expand Up @@ -2700,7 +2700,7 @@
\begin{itemdescr}
\pnum
\ensures
\tcode{get() == nullptr}.
\tcode{get() == nullptr} is \tcode{true}.

\pnum
\returns
Expand All @@ -2726,7 +2726,7 @@

\pnum
\ensures
\tcode{get() == p}.
\tcode{get() == p} is \tcode{true}.
\begin{note}
The postcondition does not hold if the call to \tcode{get_deleter()}
destroys \tcode{*this} since \tcode{this->get()} is no longer a valid expression.
Expand Down