Annex G (informative) Ill-formed, no diagnostic required [ifndr]

G.6 [dcl]: Declarations [ifndr.dcl]

G.6.4[ifndr:dcl.contract.func.mismatched.contract.specifiers]
Specified in: [dcl.contract.func]

1
#
If two different first declarations of a function (which must therefore not be reachable from one another) do not have equivalent function contract specifiers the program is ill-formed, no diagnostic required.
2
#
[Example 1: 

Translation unit #1:int f(int x) pre(x >= 0); // IFNDR, pre present, not present in the other first declaration of f int g(int x) pre(x == 0); // IFNDR, pre differs from the other first declaration of g int h(int x) pre(x <= 0); // OK, pre equivalent to pre on the other first declaration of h

Translation unit #2:int f(int x); // IFNDR, pre not present, present in the other first declaration of f int g(int x) pre(x != 0); // IFNDR, pre differs from the other first declaration of g int h(int y) pre(y <= 0); // OK, pre equivalent to pre on the other first declaration of h — end example]