Init
This commit is contained in:
215
cppdraft/dcl/contract/func.md
Normal file
215
cppdraft/dcl/contract/func.md
Normal file
@@ -0,0 +1,215 @@
|
||||
[dcl.contract.func]
|
||||
|
||||
# 9 Declarations [[dcl]](./#dcl)
|
||||
|
||||
## 9.4 Function contract specifiers [[dcl.contract]](dcl.contract#func)
|
||||
|
||||
### 9.4.1 General [dcl.contract.func]
|
||||
|
||||
[function-contract-specifier-seq:](#nt:function-contract-specifier-seq "9.4.1 General [dcl.contract.func]")
|
||||
[*function-contract-specifier*](#nt:function-contract-specifier "9.4.1 General [dcl.contract.func]") [*function-contract-specifier-seq*](#nt:function-contract-specifier-seq "9.4.1 General [dcl.contract.func]")opt
|
||||
|
||||
[function-contract-specifier:](#nt:function-contract-specifier "9.4.1 General [dcl.contract.func]")
|
||||
[*precondition-specifier*](#nt:precondition-specifier "9.4.1 General [dcl.contract.func]")
|
||||
[*postcondition-specifier*](#nt:postcondition-specifier "9.4.1 General [dcl.contract.func]")
|
||||
|
||||
[precondition-specifier:](#nt:precondition-specifier "9.4.1 General [dcl.contract.func]")
|
||||
pre [*attribute-specifier-seq*](dcl.attr.grammar#nt:attribute-specifier-seq "9.13.1 Attribute syntax and semantics [dcl.attr.grammar]")opt ( [*conditional-expression*](expr.cond#nt:conditional-expression "7.6.16 Conditional operator [expr.cond]") )
|
||||
|
||||
[postcondition-specifier:](#nt:postcondition-specifier "9.4.1 General [dcl.contract.func]")
|
||||
post [*attribute-specifier-seq*](dcl.attr.grammar#nt:attribute-specifier-seq "9.13.1 Attribute syntax and semantics [dcl.attr.grammar]")opt ( [*result-name-introducer*](dcl.contract.res#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]")opt [*conditional-expression*](expr.cond#nt:conditional-expression "7.6.16 Conditional operator [expr.cond]") )
|
||||
|
||||
[1](#1)
|
||||
|
||||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4613)
|
||||
|
||||
A [*function contract assertion*](#def:contract_assertion,function "9.4.1 General [dcl.contract.func]") is a contract assertion ([[basic.contract.general]](basic.contract.general "6.11.1 General"))
|
||||
associated with a function[.](#1.sentence-1)
|
||||
|
||||
A [*precondition-specifier*](#nt:precondition-specifier "9.4.1 General [dcl.contract.func]") introduces a [*precondition assertion*](#def:assertion,precondition "9.4.1 General [dcl.contract.func]"),
|
||||
which is a function contract assertion
|
||||
associated with entering a function[.](#1.sentence-2)
|
||||
|
||||
A [*postcondition-specifier*](#nt:postcondition-specifier "9.4.1 General [dcl.contract.func]") introduces a [*postcondition assertion*](#def:assertion,postcondition "9.4.1 General [dcl.contract.func]"),
|
||||
which is a function contract assertion
|
||||
associated with exiting a function normally[.](#1.sentence-3)
|
||||
|
||||
[*Note [1](#note-1)*:
|
||||
|
||||
A postcondition assertion
|
||||
is not associated with exiting a function
|
||||
in any other fashion,
|
||||
such as via an exception ([[expr.throw]](expr.throw "7.6.18 Throwing an exception"))
|
||||
or via a call to longjmp ([[csetjmp.syn]](csetjmp.syn "17.14.3 Header <csetjmp> synopsis"))[.](#1.sentence-4)
|
||||
|
||||
â *end note*]
|
||||
|
||||
[2](#2)
|
||||
|
||||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4635)
|
||||
|
||||
The predicate ([[basic.contract.general]](basic.contract.general "6.11.1 General"))
|
||||
of a function contract assertion
|
||||
is its [*conditional-expression*](expr.cond#nt:conditional-expression "7.6.16 Conditional operator [expr.cond]") contextually converted to bool[.](#2.sentence-1)
|
||||
|
||||
[3](#3)
|
||||
|
||||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4641)
|
||||
|
||||
Each [*function-contract-specifier*](#nt:function-contract-specifier "9.4.1 General [dcl.contract.func]") of a [*function-contract-specifier-seq*](#nt:function-contract-specifier-seq "9.4.1 General [dcl.contract.func]") (if any)
|
||||
of an unspecified first declaration ([[basic.def]](basic.def "6.2 Declarations and definitions"))
|
||||
of a function
|
||||
introduces a corresponding function contract assertion for that function[.](#3.sentence-1)
|
||||
|
||||
The optional [*attribute-specifier-seq*](dcl.attr.grammar#nt:attribute-specifier-seq "9.13.1 Attribute syntax and semantics [dcl.attr.grammar]") following pre or post appertains to the introduced contract assertion[.](#3.sentence-2)
|
||||
|
||||
[*Note [2](#note-2)*:
|
||||
|
||||
The [*function-contract-specifier-seq*](#nt:function-contract-specifier-seq "9.4.1 General [dcl.contract.func]") of a [*lambda-declarator*](expr.prim.lambda.general#nt:lambda-declarator "7.5.6.1 General [expr.prim.lambda.general]") applies to the function call operator or operator template
|
||||
of the corresponding closure type ([[expr.prim.lambda.closure]](expr.prim.lambda.closure "7.5.6.2 Closure types"))[.](#3.sentence-3)
|
||||
|
||||
â *end note*]
|
||||
|
||||
[4](#4)
|
||||
|
||||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4657)
|
||||
|
||||
A declaration D of a function or function template *f* that is not a first declaration shall have either
|
||||
no [*function-contract-specifier-seq*](#nt:function-contract-specifier-seq "9.4.1 General [dcl.contract.func]") or the same [*function-contract-specifier-seq*](#nt:function-contract-specifier-seq "9.4.1 General [dcl.contract.func]") (see below)
|
||||
as any first declaration F reachable from D[.](#4.sentence-1)
|
||||
|
||||
If D and F are
|
||||
in different translation units,
|
||||
a diagnostic is required only if D is attached to a named module[.](#4.sentence-2)
|
||||
|
||||
If a declaration F1 is a
|
||||
first declaration of f in one translation unit and
|
||||
a declaration F2 is a
|
||||
first declaration of f in another translation unit,F1 and F2 shall specify the same[*function-contract-specifier-seq*](#nt:function-contract-specifier-seq "9.4.1 General [dcl.contract.func]"), no diagnostic required[.](#4.sentence-3)
|
||||
|
||||
[5](#5)
|
||||
|
||||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4675)
|
||||
|
||||
A [*function-contract-specifier-seq*](#nt:function-contract-specifier-seq "9.4.1 General [dcl.contract.func]") S1 is the same as
|
||||
a [*function-contract-specifier-seq*](#nt:function-contract-specifier-seq "9.4.1 General [dcl.contract.func]") S2 if S1 and S2 consist of
|
||||
the same [*function-contract-specifier*](#nt:function-contract-specifier "9.4.1 General [dcl.contract.func]")*s* in the same order[.](#5.sentence-1)
|
||||
|
||||
A [*function-contract-specifier*](#nt:function-contract-specifier "9.4.1 General [dcl.contract.func]") C1 on a function declaration D1 is
|
||||
the same as
|
||||
a [*function-contract-specifier*](#nt:function-contract-specifier "9.4.1 General [dcl.contract.func]") C2 on a function declaration D2 if
|
||||
|
||||
- [(5.1)](#5.1)
|
||||
|
||||
their predicates P1 and P2 would
|
||||
satisfy the one-definition rule ([[basic.def.odr]](basic.def.odr "6.3 One-definition rule"))
|
||||
if placed in function definitions on
|
||||
the declarations D1 and D2, respectively, except for
|
||||
* [(5.1.1)](#5.1.1)
|
||||
|
||||
renaming of the parameters of *f*,
|
||||
|
||||
* [(5.1.2)](#5.1.2)
|
||||
|
||||
renaming of template parameters of
|
||||
a template enclosing , and
|
||||
|
||||
* [(5.1.3)](#5.1.3)
|
||||
|
||||
renaming of the result binding ([[dcl.contract.res]](dcl.contract.res "9.4.2 Referring to the result object")), if any,
|
||||
|
||||
and,
|
||||
if D1 and D2 are in different translation units,
|
||||
corresponding entities defined within each predicate
|
||||
behave as if there is a single entity with a single definition, and
|
||||
|
||||
- [(5.2)](#5.2)
|
||||
|
||||
both C1 and C2 specify a [*result-name-introducer*](dcl.contract.res#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") or neither do[.](#5.sentence-2)
|
||||
|
||||
If this condition is not met
|
||||
solely due to the comparison of two [*lambda-expression*](expr.prim.lambda.general#nt:lambda-expression "7.5.6.1 General [expr.prim.lambda.general]")*s* that are contained within P1 and P2,
|
||||
no diagnostic is required[.](#5.sentence-3)
|
||||
|
||||
[*Note [3](#note-3)*:
|
||||
|
||||
Equivalent[*function-contract-specifier-seq*](#nt:function-contract-specifier-seq "9.4.1 General [dcl.contract.func]")*s* apply to all uses and definitions
|
||||
of a function across all translation units[.](#5.sentence-4)
|
||||
|
||||
â *end note*]
|
||||
|
||||
[*Example [1](#example-1)*: bool b1, b2;
|
||||
|
||||
void f() pre (b1) pre ([]{ return b2; }());void f(); // OK, [*function-contract-specifier*](#nt:function-contract-specifier "9.4.1 General [dcl.contract.func]")*s* omittedvoid f() pre (b1) pre ([]{ return b2; }()); // error: closures have different types.void f() pre (b1); // error: [*function-contract-specifier*](#nt:function-contract-specifier "9.4.1 General [dcl.contract.func]")*s* only partially repeatedint g() post(r : b1);int g() post(b1); // error: mismatched [*result-name-introducer*](dcl.contract.res#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") presencenamespace N {void h() pre (b1); bool b1; void h() pre (b1); // error: [*function-contract-specifier*](#nt:function-contract-specifier "9.4.1 General [dcl.contract.func]")*s* differ according to// the one-definition rule ([[basic.def.odr]](basic.def.odr "6.3 One-definition rule")).} â *end example*]
|
||||
|
||||
[6](#6)
|
||||
|
||||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4745)
|
||||
|
||||
A virtual function ([[class.virtual]](class.virtual "11.7.3 Virtual functions")),
|
||||
a deleted function ([[dcl.fct.def.delete]](dcl.fct.def.delete "9.6.3 Deleted definitions")),
|
||||
or a function defaulted on its first declaration ([[dcl.fct.def.default]](dcl.fct.def.default "9.6.2 Explicitly-defaulted functions"))
|
||||
shall not have a [*function-contract-specifier-seq*](#nt:function-contract-specifier-seq "9.4.1 General [dcl.contract.func]")[.](#6.sentence-1)
|
||||
|
||||
[7](#7)
|
||||
|
||||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4751)
|
||||
|
||||
If the predicate of a postcondition assertion
|
||||
of a function *f* odr-uses ([[basic.def.odr]](basic.def.odr "6.3 One-definition rule"))
|
||||
a non-reference parameter of *f*,
|
||||
that parameter
|
||||
and the corresponding parameter on all declarations of *f* shall have const type[.](#7.sentence-1)
|
||||
|
||||
[*Note [4](#note-4)*:
|
||||
|
||||
This requirement applies
|
||||
even to declarations that do not specify the [*postcondition-specifier*](#nt:postcondition-specifier "9.4.1 General [dcl.contract.func]")[.](#7.sentence-2)
|
||||
|
||||
Parameters with array or function type
|
||||
will decay to non-const types
|
||||
even if a const qualifier is present[.](#7.sentence-3)
|
||||
|
||||
[*Example [2](#example-2)*: int f(const int i[10]) post(r : r == i[0]); // error: i has type const int * (not int* const). â *end example*]
|
||||
|
||||
â *end note*]
|
||||
|
||||
[8](#8)
|
||||
|
||||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4773)
|
||||
|
||||
[*Note [5](#note-5)*:
|
||||
|
||||
The function contract assertions of a function
|
||||
are evaluated even when invoked indirectly,
|
||||
such as through a pointer to function or a pointer to member function[.](#8.sentence-1)
|
||||
|
||||
A pointer to function,
|
||||
pointer to member function,
|
||||
or function type alias
|
||||
cannot have a [*function-contract-specifier-seq*](#nt:function-contract-specifier-seq "9.4.1 General [dcl.contract.func]") associated directly with it[.](#8.sentence-2)
|
||||
|
||||
â *end note*]
|
||||
|
||||
[9](#9)
|
||||
|
||||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4785)
|
||||
|
||||
The function contract assertions of a function
|
||||
are considered to be [*needed*](#def:needed,function_contract_assertion "9.4.1 General [dcl.contract.func]") ([[temp.inst]](temp.inst "13.9.2 Implicit instantiation")) when
|
||||
|
||||
- [(9.1)](#9.1)
|
||||
|
||||
the function is odr-used ([[basic.def.odr]](basic.def.odr "6.3 One-definition rule")) or
|
||||
|
||||
- [(9.2)](#9.2)
|
||||
|
||||
the function is defined[.](#9.sentence-1)
|
||||
|
||||
[*Note [6](#note-6)*:
|
||||
|
||||
Overload resolution does not consider[*function-contract-specifier*](#nt:function-contract-specifier "9.4.1 General [dcl.contract.func]")*s* ([[temp.deduct]](temp.deduct "13.10.3 Template argument deduction"), [[temp.inst]](temp.inst "13.9.2 Implicit instantiation"))[.](#9.sentence-2)
|
||||
|
||||
[*Example [3](#example-3)*: template <typename T> void f(T t) pre( t == "" );template <typename T> void f(T&& t);void g(){ f(5); // error: ambiguous} â *end example*]
|
||||
|
||||
â *end note*]
|
||||
56
cppdraft/dcl/contract/res.md
Normal file
56
cppdraft/dcl/contract/res.md
Normal file
@@ -0,0 +1,56 @@
|
||||
[dcl.contract.res]
|
||||
|
||||
# 9 Declarations [[dcl]](./#dcl)
|
||||
|
||||
## 9.4 Function contract specifiers [[dcl.contract]](dcl.contract#res)
|
||||
|
||||
### 9.4.2 Referring to the result object [dcl.contract.res]
|
||||
|
||||
[attributed-identifier:](#nt:attributed-identifier "9.4.2 Referring to the result object [dcl.contract.res]")
|
||||
[*identifier*](lex.name#nt:identifier "5.11 Identifiers [lex.name]") [*attribute-specifier-seq*](dcl.attr.grammar#nt:attribute-specifier-seq "9.13.1 Attribute syntax and semantics [dcl.attr.grammar]")opt
|
||||
|
||||
[result-name-introducer:](#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]")
|
||||
[*attributed-identifier*](#nt:attributed-identifier "9.4.2 Referring to the result object [dcl.contract.res]") :
|
||||
|
||||
[1](#1)
|
||||
|
||||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4822)
|
||||
|
||||
The [*result-name-introducer*](#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") of a [*postcondition-specifier*](dcl.contract.func#nt:postcondition-specifier "9.4.1 General [dcl.contract.func]") is a declaration[.](#1.sentence-1)
|
||||
|
||||
The [*result-name-introducer*](#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") introduces the [*identifier*](lex.name#nt:identifier "5.11 Identifiers [lex.name]") as the name of a [*result binding*](#def:result_binding "9.4.2 Referring to the result object [dcl.contract.res]") of the associated function[.](#1.sentence-2)
|
||||
|
||||
If a postcondition assertion has a [*result-name-introducer*](#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") and the return type of the function is cv void,
|
||||
the program is ill-formed[.](#1.sentence-3)
|
||||
|
||||
A result binding denotes
|
||||
the object or reference returned by
|
||||
invocation of that function[.](#1.sentence-4)
|
||||
|
||||
The type of a result binding
|
||||
is the return type of its associated function[.](#1.sentence-5)
|
||||
|
||||
The optional [*attribute-specifier-seq*](dcl.attr.grammar#nt:attribute-specifier-seq "9.13.1 Attribute syntax and semantics [dcl.attr.grammar]") of the [*attributed-identifier*](#nt:attributed-identifier "9.4.2 Referring to the result object [dcl.contract.res]") in the [*result-name-introducer*](#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") appertains to the result binding so introduced[.](#1.sentence-6)
|
||||
|
||||
[*Note [1](#note-1)*:
|
||||
|
||||
An [*id-expression*](expr.prim.id.general#nt:id-expression "7.5.5.1 General [expr.prim.id.general]") that names a result binding is a const lvalue ([[expr.prim.id.unqual]](expr.prim.id.unqual "7.5.5.2 Unqualified names"))[.](#1.sentence-7)
|
||||
|
||||
â *end note*]
|
||||
|
||||
[*Example [1](#example-1)*: int f() post(r : r == 1){return 1;}int i = f(); // Postcondition check succeeds. â *end example*]
|
||||
|
||||
[*Example [2](#example-2)*: struct A {};struct B { B() {} B(const B&) {}};
|
||||
|
||||
template <typename T> T f(T* const ptr) post(r: &r == ptr){return {};}int main() { A a = f(&a); // The postcondition check can fail if the implementation introduces// a temporary for the return value ([[class.temporary]](class.temporary "6.8.7 Temporary objects")). B b = f(&b); // The postcondition check succeeds, no temporary is introduced.} â *end example*]
|
||||
|
||||
[2](#2)
|
||||
|
||||
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/declarations.tex#L4882)
|
||||
|
||||
When the declared return type
|
||||
of a non-templated function
|
||||
contains a placeholder type,
|
||||
a [*postcondition-specifier*](dcl.contract.func#nt:postcondition-specifier "9.4.1 General [dcl.contract.func]") with a [*result-name-introducer*](#nt:result-name-introducer "9.4.2 Referring to the result object [dcl.contract.res]") shall be present only on a definition[.](#2.sentence-1)
|
||||
|
||||
[*Example [3](#example-3)*: auto g(auto&) post (r: r >= 0); // OK, g is a template.auto h() post (r: r >= 0); // error: cannot name the return valueauto k() post (r: r >= 0) // OK{return 0;} â *end example*]
|
||||
Reference in New Issue
Block a user