From bd766dd85bc42eda8126f12ef7514671540b0682 Mon Sep 17 00:00:00 2001 From: kirtchev-adacore Date: Wed, 1 Jul 2026 10:49:57 +0300 Subject: [PATCH 1/3] [1.95.0] Document provenance and its use in const eval The information has been taken from - [core::ptr Provenance](https://doc.rust-lang.org/core/ptr/index.html#provenance) - [reference#2091](https://github.com/rust-lang/reference/pull/2091) - [reference#2139](https://github.com/rust-lang/reference/pull/2138) --- src/changelog.rst | 3 +++ src/glossary.rst | 28 ++++++++++++++++++++++-- src/types-and-traits.rst | 9 ++++---- src/unsafety.rst | 2 +- src/values.rst | 47 +++++++++++++++++++++++++++++++++++++++- 5 files changed, 81 insertions(+), 8 deletions(-) diff --git a/src/changelog.rst b/src/changelog.rst index bdd47665..4f26228a 100644 --- a/src/changelog.rst +++ b/src/changelog.rst @@ -136,6 +136,9 @@ Language changes in Rust 1.95.0 - The target is outside the scope of the FLS. - `const-eval: be more consistent in the behavior of padding during typed copies `_ + + - TODO: Fill out once we settle on the rules. + - `Const blocks are no longer evaluated to determine if expressions involving fallible operations can implicitly be constant-promoted `_ - This implementation-specifc behavior is outside the scope of the FLS. diff --git a/src/glossary.rst b/src/glossary.rst index c6fc3abe..71984a34 100644 --- a/src/glossary.rst +++ b/src/glossary.rst @@ -1156,6 +1156,11 @@ A :dt:`derive macro` is a :t:`procedural macro` that consumes a stream of :t:`[token]s` and produces a stream of tokens, and is invoked via attribute :c:`derive`. +derived indirection value +^^^^^^^^^^^^^^^^^^^^^^^^^ + +A :dt:`derived indirection value` is an :t:`indirection value` obtained by performing address or pointer arithmetic on another :t:`indirection value`. + destruction ^^^^^^^^^^^ @@ -2193,6 +2198,11 @@ indirection type An :dt:`indirection type` is a :t:`type` whose :t:`[value]s` refer to memory locations. +indirection value +^^^^^^^^^^^^^^^^^ + +An :dt:`indirection value` is either a :t:`raw pointer` or a :t:`reference`. + inert attribute ^^^^^^^^^^^^^^^ @@ -3186,7 +3196,6 @@ opt-out trait bound An :dt:`opt-out trait bound` is a :t:`trait bound` with :s:`Punctuation` ``?`` that nullifies an implicitly added :t:`trait bound`. - or-pattern ^^^^^^^^^^ @@ -3194,6 +3203,11 @@ An :dt:`or-pattern` is a :t:`pattern` that matches on one of two or more :t:`[pa See :s:`Pattern`. +original indirection value +^^^^^^^^^^^^^^^^^^^^^^^^^^ + +An :dt:`original indirection value` is an :t:`indirection value` created via allocation. + outer attribute ^^^^^^^^^^^^^^^ @@ -3476,6 +3490,11 @@ program entry point A :dt:`program entry point` is a :t:`function` that is invoked at the start of a Rust program. +provenance +^^^^^^^^^^ + +:dt:`Provenance` is an optional property of :t:`[indirection value]s` that restricts the addresses an :t:`indirection value` may point to, the timespan during which the :t:`indirection value` may point to those addresses, and whether the :t:`indirection value` can read from and write to those addresses. + public visibility ^^^^^^^^^^^^^^^^^ @@ -3659,7 +3678,7 @@ See :s:`RawCStringLiteral`. raw pointer ^^^^^^^^^^^ -A :dt:`raw pointer` is a pointer of a :t:`raw pointer type`. +A :dt:`raw pointer` is a :t:`value` of a :t:`raw pointer type`. raw pointer type ^^^^^^^^^^^^^^^^ @@ -5195,6 +5214,11 @@ context. See :s:`WeakKeyword`. +well-formed indirection value +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +A :dt:`well-formed indirection value` is an :t:`indirection value` with :t:`provenance`, where all bytes that comprise the :t:`indirection value` are initialized, correctly ordered, and are fragments of the same :t:`original indirection value`. + where clause ^^^^^^^^^^^^ diff --git a/src/types-and-traits.rst b/src/types-and-traits.rst index f142329d..98d4d9ca 100644 --- a/src/types-and-traits.rst +++ b/src/types-and-traits.rst @@ -1028,13 +1028,14 @@ A :t:`mutable raw pointer type` is a :t:`raw pointer type` subject to An :t:`immutable raw pointer type` is a :t:`raw pointer type` subject to :t:`keyword` ``const``. +:dp:`fls_c2Guy3fPYaUV` +A :t:`raw pointer` is a :t:`value` of a :t:`raw pointer type`. + :dp:`fls_hrum767l6dte` -Comparing two :t:`[value]s` of :t:`[raw pointer type]s` compares the addresses -of the :t:`[value]s`. +Comparing two :t:`[raw pointer]s` compares the addresses of the :t:`[raw pointer]s`. :dp:`fls_k6ues2936pjq` -Comparing a :t:`value` of a :t:`raw pointer type` to a :t:`value` of a -:t:`dynamically sized type` compares the data being pointed to. +Comparing a :t:`raw pointer` to a :t:`value` of a :t:`dynamically sized type` compares the data being pointed to. .. rubric:: Examples diff --git a/src/unsafety.rst b/src/unsafety.rst index 1ede11bd..47cb8e7a 100644 --- a/src/unsafety.rst +++ b/src/unsafety.rst @@ -23,7 +23,7 @@ An :t:`unsafe operation` is an operation that may result in The :t:`[unsafe operation]s` are: * :dp:`fls_jd1inwz7ulyw` - Dereferencing a :t:`value` of a :t:`raw pointer type`. + Dereferencing a :t:`raw pointer`. * :dp:`fls_3ra8s1v1vbek` Reading or writing an :t:`external static`. diff --git a/src/values.rst b/src/values.rst index 68c27eb5..5224dd22 100644 --- a/src/values.rst +++ b/src/values.rst @@ -42,6 +42,15 @@ Two :t:`[value]s` :t:`overlap` when * :dp:`fls_eoak5mdl6ma` Both :t:`[value]s` are elements of the same :t:`array`. +:dp:`fls_jriT46yWgIR0` +An :t:`indirection value` is either a :t:`raw pointer` or a :t:`reference`. + +:dp:`fls_VWUlxTy0QF9d` +An :t:`original indirection value` is an :t:`indirection value` created via allocation. + +:dp:`fls_kaPNJ7iIHPro` +A :t:`derived indirection value` is an :t:`indirection value` obtained by performing address or pointer arithmetic on another :t:`indirection value`. + .. rubric:: Undefined Behavior :dp:`fls_6lg0oaaopc26` @@ -108,9 +117,12 @@ The :t:`expression` of a :t:`constant initializer` shall be a :t:`constant expression`. :dp:`fls_deuo1pn8cjd6` -The value of a :t:`constant` is determined by evaluating its +The :t:`value` of a :t:`constant` is determined by evaluating its :t:`constant initializer`. +:dp:`fls_l1FOH8zt0XRZ` +If the :t:`value` produced by evaluating a :t:`constant initializer` denotes an :t:`indirection value`, then the :t:`value` shall be a :t:`well-formed indirection value`. + .. rubric:: Dynamic Semantics :dp:`fls_xezt9hl069h4` @@ -188,6 +200,12 @@ A :t:`static` shall have a :t:`static initializer`, unless it is an The :t:`expression` of a :t:`static initializer` shall be a :t:`constant expression`. +:dp:`fls_41zoQ54MiLMm` +The :t:`static` is determined by evaluating its :t:`static initializer`. + +:dp:`fls_37oocZVDne5Y` +If the :t:`value` produced by evaluating a :t:`static initializer` denotes an :t:`indirection value`, then the :t:`value` shall be a :t:`well-formed indirection value`. + :dp:`fls_8dcldbvu7lav` A use of a :t:`static` is a :t:`place expression` referring to the unique location of the :t:`static`. @@ -306,3 +324,30 @@ promoting the produced :t:`mutable borrow` to have ``'static`` :t:`lifetime`. #. :dp:`fls_ap85svxyuhvg` The :t:`value` of the anonymous :t:`constant` is :t:`borrowed` with ``'static`` :t:`lifetime`. + +.. _fls_Dqk4eIvxHloY: + +Provenance +---------- + +.. rubric:: Legality Rules + +:dp:`fls_5MkKtNL9oCsL` +:t:`Provenance` is an optional property of :t:`[indirection value]s` that restricts the addresses an :t:`indirection value` may point to, the timespan during which the :t:`indirection value` may point to those addresses, and whether the :t:`indirection value` can read from and write to those addresses. + +:dp:`fls_1NJhTBN1D2qv` +An :t:`original indirection value` always carries :t:`provenance`. + +:dp:`fls_wnJmQYT7iKQf` +A :t:`derived indirection value` inherits the :t:`provenance` of the :t:`indirection value` it was created from, if any. + +:dp:`fls_ffh8mAkebORJ` +A :t:`well-formed indirection value` is an :t:`indirection value` with :t:`provenance`, where all bytes that comprise the :t:`indirection value` are initialized, correctly ordered, and are fragments of the same :t:`original indirection value`. + +.. rubric:: Undefined Behavior + +:dp:`fls_c3DaCLQEBpYQ` +It is undefined behavior to access memory through an :t:`indirection value` which does not have :t:`provenance` over that memory. + +:dp:`fls_MwDoxVPRZCqm` +It is undefined behavior to offset an :t:`indirection value` beyond the bounds of the memory block it has :t:`provenance` over. From a8393ef30e197c134f32968cd6ae507fbb010f81 Mon Sep 17 00:00:00 2001 From: kirtchev-adacore Date: Wed, 8 Jul 2026 10:19:08 +0300 Subject: [PATCH 2/3] Use "pointer" terminology --- src/glossary.rst | 27 +++++++++++---------------- src/types-and-traits.rst | 5 +++++ src/values.rst | 22 +++++++++++----------- 3 files changed, 27 insertions(+), 27 deletions(-) diff --git a/src/glossary.rst b/src/glossary.rst index 71984a34..752abb56 100644 --- a/src/glossary.rst +++ b/src/glossary.rst @@ -1156,10 +1156,10 @@ A :dt:`derive macro` is a :t:`procedural macro` that consumes a stream of :t:`[token]s` and produces a stream of tokens, and is invoked via attribute :c:`derive`. -derived indirection value -^^^^^^^^^^^^^^^^^^^^^^^^^ +derived pointer +^^^^^^^^^^^^^^^ -A :dt:`derived indirection value` is an :t:`indirection value` obtained by performing address or pointer arithmetic on another :t:`indirection value`. +A :dt:`derived pointer` is a :t:`pointer` obtained by performing address or pointer arithmetic on another :t:`pointer`. destruction ^^^^^^^^^^^ @@ -2198,11 +2198,6 @@ indirection type An :dt:`indirection type` is a :t:`type` whose :t:`[value]s` refer to memory locations. -indirection value -^^^^^^^^^^^^^^^^^ - -An :dt:`indirection value` is either a :t:`raw pointer` or a :t:`reference`. - inert attribute ^^^^^^^^^^^^^^^ @@ -3203,10 +3198,10 @@ An :dt:`or-pattern` is a :t:`pattern` that matches on one of two or more :t:`[pa See :s:`Pattern`. -original indirection value -^^^^^^^^^^^^^^^^^^^^^^^^^^ +original pointer +^^^^^^^^^^^^^^^^ -An :dt:`original indirection value` is an :t:`indirection value` created via allocation. +An :dt:`original pointer` is a :t:`pointer` created via allocation. outer attribute ^^^^^^^^^^^^^^^ @@ -3425,7 +3420,7 @@ A :dt:`pointer` is a :t:`value` of a :t:`pointer type`. pointer type ^^^^^^^^^^^^ -A :dt:`pointer type` is a :t:`type` whose values indicate memory locations. +A :dt:`pointer type` is a :t:`type` whose :t:`[value]s` indicate memory locations. positional register argument ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -3493,7 +3488,7 @@ a Rust program. provenance ^^^^^^^^^^ -:dt:`Provenance` is an optional property of :t:`[indirection value]s` that restricts the addresses an :t:`indirection value` may point to, the timespan during which the :t:`indirection value` may point to those addresses, and whether the :t:`indirection value` can read from and write to those addresses. +:dt:`Provenance` is an optional property of :t:`[pointer]s` that restricts the addresses a :t:`pointer` may point to, the timespan during which the :t:`pointer` may point to those addresses, and whether the :t:`pointer` can read from and write to those addresses. public visibility ^^^^^^^^^^^^^^^^^ @@ -5214,10 +5209,10 @@ context. See :s:`WeakKeyword`. -well-formed indirection value -^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +well-formed pointer +^^^^^^^^^^^^^^^^^^^ -A :dt:`well-formed indirection value` is an :t:`indirection value` with :t:`provenance`, where all bytes that comprise the :t:`indirection value` are initialized, correctly ordered, and are fragments of the same :t:`original indirection value`. +A :dt:`well-formed pointer` is a :t:`pointer` with :t:`provenance`, where all bytes that comprise the :t:`pointer` are initialized, correctly ordered, and are fragments of the same :t:`original pointer`. where clause ^^^^^^^^^^^^ diff --git a/src/types-and-traits.rst b/src/types-and-traits.rst index 98d4d9ca..54ba0d8a 100644 --- a/src/types-and-traits.rst +++ b/src/types-and-traits.rst @@ -939,6 +939,11 @@ A :t:`function item type` implements the :std:`core::ops::Fn` :t:`trait`, the :s Indirection Types ----------------- +.. rubric:: Legality Rules + +:dp:`fls_3qI8FXMsyk0f` +A :t:`pointer type` is a :t:`type` whose :t:`[value]s` indicate memory locations. + .. _fls_xztr1kebz8bo: Function Pointer Types diff --git a/src/values.rst b/src/values.rst index 5224dd22..01d1ebec 100644 --- a/src/values.rst +++ b/src/values.rst @@ -43,13 +43,13 @@ Two :t:`[value]s` :t:`overlap` when Both :t:`[value]s` are elements of the same :t:`array`. :dp:`fls_jriT46yWgIR0` -An :t:`indirection value` is either a :t:`raw pointer` or a :t:`reference`. +A :t:`pointer` is a :t:`value` of a :t:`pointer type`. :dp:`fls_VWUlxTy0QF9d` -An :t:`original indirection value` is an :t:`indirection value` created via allocation. +An :t:`original pointer` is a :t:`pointer` created via allocation. :dp:`fls_kaPNJ7iIHPro` -A :t:`derived indirection value` is an :t:`indirection value` obtained by performing address or pointer arithmetic on another :t:`indirection value`. +A :t:`derived pointer` is a :t:`pointer` obtained by performing address or pointer arithmetic on another :t:`pointer`. .. rubric:: Undefined Behavior @@ -121,7 +121,7 @@ The :t:`value` of a :t:`constant` is determined by evaluating its :t:`constant initializer`. :dp:`fls_l1FOH8zt0XRZ` -If the :t:`value` produced by evaluating a :t:`constant initializer` denotes an :t:`indirection value`, then the :t:`value` shall be a :t:`well-formed indirection value`. +If the :t:`value` produced by evaluating a :t:`constant initializer` is a :t:`pointer`, then the :t:`pointer` shall be a :t:`well-formed pointer`. .. rubric:: Dynamic Semantics @@ -204,7 +204,7 @@ The :t:`expression` of a :t:`static initializer` shall be a The :t:`static` is determined by evaluating its :t:`static initializer`. :dp:`fls_37oocZVDne5Y` -If the :t:`value` produced by evaluating a :t:`static initializer` denotes an :t:`indirection value`, then the :t:`value` shall be a :t:`well-formed indirection value`. +If the :t:`value` produced by evaluating a :t:`static initializer` is a :t:`pointer`, then the :t:`pointer` shall be a :t:`well-formed pointer`. :dp:`fls_8dcldbvu7lav` A use of a :t:`static` is a :t:`place expression` referring to the unique @@ -333,21 +333,21 @@ Provenance .. rubric:: Legality Rules :dp:`fls_5MkKtNL9oCsL` -:t:`Provenance` is an optional property of :t:`[indirection value]s` that restricts the addresses an :t:`indirection value` may point to, the timespan during which the :t:`indirection value` may point to those addresses, and whether the :t:`indirection value` can read from and write to those addresses. +:t:`Provenance` is an optional property of :t:`[pointer]s` that restricts the addresses a :t:`pointer` may point to, the timespan during which the :t:`pointer` may point to those addresses, and whether the :t:`pointer` can read from and write to those addresses. :dp:`fls_1NJhTBN1D2qv` -An :t:`original indirection value` always carries :t:`provenance`. +An :t:`original pointer` always carries :t:`provenance`. :dp:`fls_wnJmQYT7iKQf` -A :t:`derived indirection value` inherits the :t:`provenance` of the :t:`indirection value` it was created from, if any. +A :t:`derived pointer` inherits the :t:`provenance` of the :t:`pointer` it was created from, if any. :dp:`fls_ffh8mAkebORJ` -A :t:`well-formed indirection value` is an :t:`indirection value` with :t:`provenance`, where all bytes that comprise the :t:`indirection value` are initialized, correctly ordered, and are fragments of the same :t:`original indirection value`. +A :t:`well-formed pointer` is a :t:`pointer` with :t:`provenance`, where all bytes that comprise the :t:`pointer` are initialized, correctly ordered, and are fragments of the same :t:`original pointer`. .. rubric:: Undefined Behavior :dp:`fls_c3DaCLQEBpYQ` -It is undefined behavior to access memory through an :t:`indirection value` which does not have :t:`provenance` over that memory. +It is undefined behavior to access memory through a :t:`pointer` which does not have :t:`provenance` over that memory. :dp:`fls_MwDoxVPRZCqm` -It is undefined behavior to offset an :t:`indirection value` beyond the bounds of the memory block it has :t:`provenance` over. +It is undefined behavior to offset a :t:`pointer` beyond the bounds of the memory block it has :t:`provenance` over. From 979328b4c2722253a8b61385af3aa69d78d50431 Mon Sep 17 00:00:00 2001 From: kirtchev-adacore Date: Thu, 9 Jul 2026 11:45:29 +0300 Subject: [PATCH 3/3] Address Pete's review from 2026-07-08 --- src/glossary.rst | 8 ++-- src/types-and-traits.rst | 2 +- src/values.rst | 80 ++++++++++++++++++---------------------- 3 files changed, 40 insertions(+), 50 deletions(-) diff --git a/src/glossary.rst b/src/glossary.rst index 752abb56..6412d02c 100644 --- a/src/glossary.rst +++ b/src/glossary.rst @@ -1159,7 +1159,7 @@ A :dt:`derive macro` is a :t:`procedural macro` that consumes a stream of derived pointer ^^^^^^^^^^^^^^^ -A :dt:`derived pointer` is a :t:`pointer` obtained by performing address or pointer arithmetic on another :t:`pointer`. +A :dt:`derived pointer` is a :t:`pointer` obtained by :t:`borrowing`, copying a :t:`pointer`, loading a stored :t:`pointer`, performing :t:`pointer` arithmetic, or :t:`casting` a :t:`pointer`. destruction ^^^^^^^^^^^ @@ -3420,7 +3420,7 @@ A :dt:`pointer` is a :t:`value` of a :t:`pointer type`. pointer type ^^^^^^^^^^^^ -A :dt:`pointer type` is a :t:`type` whose :t:`[value]s` indicate memory locations. +A :dt:`pointer type` is either a :t:`raw pointer type` or a :t:`reference type`. positional register argument ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -3488,7 +3488,7 @@ a Rust program. provenance ^^^^^^^^^^ -:dt:`Provenance` is an optional property of :t:`[pointer]s` that restricts the addresses a :t:`pointer` may point to, the timespan during which the :t:`pointer` may point to those addresses, and whether the :t:`pointer` can read from and write to those addresses. +:dt:`Provenance` is an optional property of :t:`[pointer]s` that restricts the memory locations the :t:`pointer` may access, the timespan during which the accesses may occur, and whether the accesses may read from or write to memory. public visibility ^^^^^^^^^^^^^^^^^ @@ -5212,7 +5212,7 @@ See :s:`WeakKeyword`. well-formed pointer ^^^^^^^^^^^^^^^^^^^ -A :dt:`well-formed pointer` is a :t:`pointer` with :t:`provenance`, where all bytes that comprise the :t:`pointer` are initialized, correctly ordered, and are fragments of the same :t:`original pointer`. +A :dt:`well-formed pointer` is a :t:`pointer` where either no byte of the :t:`pointer` carries :t:`provenance`, or every byte of the :t:`pointer` is the corresponding byte of a single :t:`pointer` with :t:`provenance`. where clause ^^^^^^^^^^^^ diff --git a/src/types-and-traits.rst b/src/types-and-traits.rst index 54ba0d8a..e6559dda 100644 --- a/src/types-and-traits.rst +++ b/src/types-and-traits.rst @@ -942,7 +942,7 @@ Indirection Types .. rubric:: Legality Rules :dp:`fls_3qI8FXMsyk0f` -A :t:`pointer type` is a :t:`type` whose :t:`[value]s` indicate memory locations. +A :t:`pointer type` is either a :t:`raw pointer type` or a :t:`reference type`. .. _fls_xztr1kebz8bo: diff --git a/src/values.rst b/src/values.rst index 01d1ebec..796c30bd 100644 --- a/src/values.rst +++ b/src/values.rst @@ -42,15 +42,6 @@ Two :t:`[value]s` :t:`overlap` when * :dp:`fls_eoak5mdl6ma` Both :t:`[value]s` are elements of the same :t:`array`. -:dp:`fls_jriT46yWgIR0` -A :t:`pointer` is a :t:`value` of a :t:`pointer type`. - -:dp:`fls_VWUlxTy0QF9d` -An :t:`original pointer` is a :t:`pointer` created via allocation. - -:dp:`fls_kaPNJ7iIHPro` -A :t:`derived pointer` is a :t:`pointer` obtained by performing address or pointer arithmetic on another :t:`pointer`. - .. rubric:: Undefined Behavior :dp:`fls_6lg0oaaopc26` @@ -71,6 +62,39 @@ It is undefined behavior to create an :t:`allocated object` with :t:`memory size` ``size`` where ``size`` is greater than the architectures maximum :c:`isize` value. +.. _fls_Dqk4eIvxHloY: + +Provenance +---------- + +.. rubric:: Legality Rules + +:dp:`fls_jriT46yWgIR0` +A :t:`pointer` is a :t:`value` of a :t:`pointer type`. + +:dp:`fls_VWUlxTy0QF9d` +An :t:`original pointer` is a :t:`pointer` created via allocation. + +:dp:`fls_kaPNJ7iIHPro` +A :t:`derived pointer` is a :t:`pointer` obtained by :t:`borrowing`, copying a :t:`pointer`, loading a stored :t:`pointer`, performing :t:`pointer` arithmetic, or :t:`casting` a :t:`pointer`. + +:dp:`fls_5MkKtNL9oCsL` +:t:`Provenance` is an optional property of :t:`[pointer]s` that restricts the memory locations the :t:`pointer` may access, the timespan during which the accesses may occur, and whether the accesses may read from or write to memory. + +:dp:`fls_1NJhTBN1D2qv` +An :t:`original pointer` carries :t:`provenance` over all or part of the :t:`allocated object` it was created from. + +:dp:`fls_wnJmQYT7iKQf` +A :t:`derived pointer` inherits the :t:`provenance` of the :t:`pointer` it was created from, if any. + +:dp:`fls_ffh8mAkebORJ` +A :t:`well-formed pointer` is a :t:`pointer` where either no byte of the :t:`pointer` carries :t:`provenance`, or every byte of the :t:`pointer` is the corresponding byte of a single :t:`pointer` with :t:`provenance`. + +.. rubric:: Undefined Behavior + +:dp:`fls_c3DaCLQEBpYQ` +It is undefined behavior to access memory through a :t:`pointer` that does not have :t:`provenance` permitting the access. + .. _fls_ixjc5jaamx84: Constants @@ -116,12 +140,8 @@ A :t:`constant` shall have a :t:`constant initializer`, unless it is an The :t:`expression` of a :t:`constant initializer` shall be a :t:`constant expression`. -:dp:`fls_deuo1pn8cjd6` -The :t:`value` of a :t:`constant` is determined by evaluating its -:t:`constant initializer`. - :dp:`fls_l1FOH8zt0XRZ` -If the :t:`value` produced by evaluating a :t:`constant initializer` is a :t:`pointer`, then the :t:`pointer` shall be a :t:`well-formed pointer`. +If the :t:`value` produced by evaluating a :t:`constant initializer` is or contains a :t:`pointer`, then each such :t:`pointer` shall be a :t:`well-formed pointer`. .. rubric:: Dynamic Semantics @@ -200,11 +220,8 @@ A :t:`static` shall have a :t:`static initializer`, unless it is an The :t:`expression` of a :t:`static initializer` shall be a :t:`constant expression`. -:dp:`fls_41zoQ54MiLMm` -The :t:`static` is determined by evaluating its :t:`static initializer`. - :dp:`fls_37oocZVDne5Y` -If the :t:`value` produced by evaluating a :t:`static initializer` is a :t:`pointer`, then the :t:`pointer` shall be a :t:`well-formed pointer`. +If the :t:`value` produced by evaluating a :t:`static initializer` is or contains a :t:`pointer`, then each such :t:`pointer` shall be a :t:`well-formed pointer`. :dp:`fls_8dcldbvu7lav` A use of a :t:`static` is a :t:`place expression` referring to the unique @@ -324,30 +341,3 @@ promoting the produced :t:`mutable borrow` to have ``'static`` :t:`lifetime`. #. :dp:`fls_ap85svxyuhvg` The :t:`value` of the anonymous :t:`constant` is :t:`borrowed` with ``'static`` :t:`lifetime`. - -.. _fls_Dqk4eIvxHloY: - -Provenance ----------- - -.. rubric:: Legality Rules - -:dp:`fls_5MkKtNL9oCsL` -:t:`Provenance` is an optional property of :t:`[pointer]s` that restricts the addresses a :t:`pointer` may point to, the timespan during which the :t:`pointer` may point to those addresses, and whether the :t:`pointer` can read from and write to those addresses. - -:dp:`fls_1NJhTBN1D2qv` -An :t:`original pointer` always carries :t:`provenance`. - -:dp:`fls_wnJmQYT7iKQf` -A :t:`derived pointer` inherits the :t:`provenance` of the :t:`pointer` it was created from, if any. - -:dp:`fls_ffh8mAkebORJ` -A :t:`well-formed pointer` is a :t:`pointer` with :t:`provenance`, where all bytes that comprise the :t:`pointer` are initialized, correctly ordered, and are fragments of the same :t:`original pointer`. - -.. rubric:: Undefined Behavior - -:dp:`fls_c3DaCLQEBpYQ` -It is undefined behavior to access memory through a :t:`pointer` which does not have :t:`provenance` over that memory. - -:dp:`fls_MwDoxVPRZCqm` -It is undefined behavior to offset a :t:`pointer` beyond the bounds of the memory block it has :t:`provenance` over.