Interfaces with contracts alongside Annex K

Jens Gustedt, INRIA and ICube, France

2026-07-13

target

preliminary discussion for possible integration into IS ISO/IEC 9899:202y

document history

document number date comment
3930 202607 Original proposal
document number title
n3929 C semantics for contracts

license

CC BY, see https://creativecommons.org/licenses/by/4.0

1 Motivation

A lot of effort had been put into the definition of the interfaces in Annex K, as to provide remplacements for C library functions that have much less cases of undefined behavior. Unfortunately there has been a lot of dispute about design decision thereafter, which had the effect that these interfaces are not used much and are even not implemented in large parts of the C community.

C has much progressed since C11 when Annex K was introduced, and some of the erroneous behavior that Annex K tried to identify at runtime, can now be formulated in carefully designed interfaces (in particular with [static n] parameter declarations). These properties are nowadays often spotted by optimizing compilers if only the declaration order of array length parameters and the corresponding array can be adapted. Nevertheless, normatively a [static n] specification still only places an errorneous call into the UB-realm, so there nothing is gained in the galactic battle between UB versus erroneous behavior.

Contracts are meant to add another level of specification to function declarations that is capable to cover much of what Annex K expresses as runtime constraints. Most importantly, contracts are visible in the function interface and thus with this tool we are able to transform UB into well-defined erroneous behavior. Additionally, contracts can be checked at caller or callee side of a function call; they can in many cases be inferred at translation time from the context and effectively be optimized out by state-of-the-art optimizers.

In this paper, we provide alternative interfaces to the interfaces in Annex K that provide the functionality of the corresponding C library call

Additionally, this paper also serves to provide a lot of examples for functions with contracts. In particular it also shows how the feature to define “ghost states” comes in handy when declaring more complicated interfaces.

In this paper we folllow a bit of a mix of the semantics between the traditional C library functions and Annex K functions. In particular, we do not use the errno_t addtion of Annex K, because for contracts (that are supposed to terminate in case of an error) only the non-erroneous execution path is accounted for. Also, there are some seemingly random differences in semantics between these two sets of functions; we try to priviledge the specification that leads to safer code.

2 Possible implementation

Since the interfaces that are proposed here are directly mirroring standard C library features, once a platform has contracts most of them can be implemented as simple inline wrappers around the corresponding C library function.

As a first example that only performs some simple checks on pointer arguments:

inline
int stdc_vfprintf(
    FILE * restrict stream,
    const char * restrict format,
    va_list arg)
        _Pre(stream) _Pre(format)
    {
        return vfprintf(stream, format, arg);
    }

Similarly, the vfprintf function can be used to implement the corresponding function with a ... argument.

inline
int stdc_fprintf(
    FILE * restrict stream,
    const char * restrict format,
    ...)
        _Pre(stream) _Pre(format)
    {
        va_list ap;
        va_start(ap);
        _Defer va_end(ap);
        return vfprintf(stream, format, ap);
    }

A more complicated example would be stdc_strcpy. To be in line with the runtime constraints of the corresponding strcpy_s we have to

inline
char* stdc_strcpy(
    size_t dstmax,
    char dst[restrict static dstmax],
    const char src[restrict static 1])
        _Pre(dst) _Pre(src)
        _Pre(dstmax) _Pre(dstmax <= STDC_MBS_MAX)
        _Pre(size_t srclen = stdc_strnlen(dstmax, src); srclen < dstmax)
        // srclen is less than STDC_MBS_MAX,
        // so the addition does not overflow
        _Pre(size_t srcmax = srclen+1; true)
        _Pre(stdc_brange_check2(srcmax, dst, srcmax, src))
        _Post(!dst[srclen])
        _Post(_ReturnValue == dst)
        [[unsequenced]] {
    return strcpy(dst, src);
}

Similarly for stdc_strncpy we have to

inline
char* stdc_strncpy(
    size_t dstmax,
    char dst[restrict static dstmax],
    const char src[restrict static 1],
    size_t n)
        _Pre(dst) _Pre(src)
        _Pre(dstmax) _Pre(dstmax <= STDC_MBS_MAX)
        _Pre(n <= dstmax)
        _Pre(size_t srclen   = strnlen(n, src); true)
        // srclen is less than STDC_MBS_MAX,
        // so the addition does not overflow
        _Pre(size_t srcmax = srclen+1; true)
        _Pre(brange_check2(n, dst, stdc_min(srcmax, n), src))
        _Post(srclen == n || !dst[srclen])
        _Post(_ReturnValue == dst)
        [[unsequenced]] {
    return strncpy(dst, src, n);
}

3 The <stdc_contracts_lib.h> header

The <stdc_contracts_lib.h> header includes the headers

It defines the following macros:

#define STDC_MBS_MAX                              // same as RSIZE_MAX
#define STDC_WCS_MAX STDC_MBS_MAX/sizeof(wchar_t)

To name the error return values with type size_t of several standard library functions consistently we use an enumeration with fixed underlying type.

enum stdc_err : size_t {
    stdc_err_none   = 0,
    stdc_err_min    = -3,
    stdc_err_next   = -3,
    stdc_err_incomp = -2,
    stdc_err_enc    = -1,
    stdc_err_notf   = -1,
};
typedef enum stdc_err stdc_err;

Then the header specifies several functions as in the following subclauses. In general, for a function named stdc_FUNCNAME the function implements the functionality of the function FUNCNAME (as given by this document) and by using contracts for the runtime constraints that are formulated for the FUNCNAME_s function in Annex K.

In the following we assume that STDC_MBS_MAX is at most SIZE_MAX/2 such that the addition of two object sizes will not overflow.

3.1 Functions handling multi-byte strings and byte arrays

As long as we do not have void[] and void const[] parameter arrays, we assume that functions with such parameter types are emulated with replacements that have char[] and char const[] parameters, and that we have macros that handle argument to parameter type conversion. This concerns

#define stdc_brange_check2(AMAX, A, BMAX, B)                             \
    stdc_brange_check2(AMAX, (void const*)A,                             \
    BMAX, (void const*)B)
#define stdc_brange_check3(AMAX, A, BMAX, B, CMAX, C)                    \
    stdc_brange_check3(AMAX, (void const*)A,                             \
    BMAX, (void const*)B,                                                \
    CMAX, (void const*)C)
#define stdc_brange_check4(AMAX, A, BMAX, B, CMAX, C, DMAX, D)           \
    stdc_brange_check4(AMAX, (void const*)A,                             \
    BMAX, (void const*)B,                                                \
    CMAX, (void const*)C,                                                \
    DMAX, (void const*)D)
#define stdc_memcpy(S1MAX, S1, N, S2)                                    \
    stdc_memcpy(S1MAX, (void*){ S1 }, N, (void const*){ S2 })
#define stdc_memmove(S1MAX, S1, N, S2)                                   \
    stdc_memmove(S1MAX, (void*){ S1 }, N, (void const*){ S2 })

3.1.1 Functions used to express predicates

These are additional functions with possibly no equivalend in Annex K that are used to express predicates. They have the attribute [[unsequenced]] such that evaluation of checks can easily be moved around by an optimizing compiler.

3.1.1.1 The stdc_brange_check functions

These function check if the byte arrays are mutually disjoint. For exampe for stdc_brange_check2 if a and b point to valid objects aObj and bObj, and if amax and bmax are not greater than sizeof(aObj) or sizeof(bObj), a call always has defined behavior.

bool stdc_brange_check2(
    size_t amax,
    void const a[static amax],
    size_t bmax,
    void const b[static bmax])
    _Pre(a) _Pre(b)
    [[unsequenced]];
bool stdc_brange_check3(
    size_t amax,
    void const a[static amax],
    size_t bmax,
    void const b[static bmax],
    size_t cmax,
    void const c[static cmax])
    _Pre(a) _Pre(b) _Pre(c)
    [[unsequenced]];
bool stdc_brange_check4(
    size_t amax,
    void const a[static amax],
    size_t bmax,
    void const b[static bmax],
    size_t cmax,
    void const c[static cmax],
    size_t dmax,
    void const d[static dmax])
    _Pre(a) _Pre(b) _Pre(c) _Pre(d)
    [[unsequenced]];

On implementations that have uintptr_t with the right properties, the body of stdc_brange_check2 could look as follows. This could easily be provided as an inline function, but would probably best be implemented as a builtin.

{
     return
         ((uintptr_t)((char const*)b + bmax) <= (uintptr_t)a)
         || ((uintptr_t)((char const*)a + amax) <= (uintptr_t)b);
}

3.1.1.2 The stdc_strnlen function

This function checks for the first position of a null character in the character array, if any. If s is a null pointer or points to a valid object Obj and if maxsize is not greater than sizeof(Obj) a call always has defined behavior.

size_t stdc_strnlen(
    size_t maxsize,
    const char *s)
        _Post(s || !_ReturnValue)
        _Post(_ReturnValue <= maxsize)
        _Post(!_ReturnValue || maxsize)
        _Post(_ReturnValue || !s || !maxsize || !s[0])
        _Post((_ReturnValue == maxsize) || !s[_ReturnValue])
        [[unsequenced]];

3.1.1.3 The stdc_ismbs function

This additional function checks if the character array is a valid string or not. If s is a null pointer or points to a valid object Obj and if maxsize is not greater than sizeof(Obj) a call always has defined behavior.

bool stdc_ismbs(
    size_t maxsize
    const char s[static maxsize ? maxsize : 1])
    [[unsequenced]];

The body of this function could look as follows. This could easily be provided as an inline function.

{
        if (!maxsize || !s) return false;
        else return !s[0] || (stdc_strnlen(maxsize, s) < maxsize);
}

3.1.2 Format functions with variable argument list

int stdc_vfprintf(
    FILE * restrict stream,
    const char * restrict format,
    …)
        _Pre(stream) _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vfscanf(
    FILE * restrict stream,
    const char * restrict format,
    …)
        _Pre(stream) _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vprintf(
    const char * restrict format,
    …)
        _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vscanf(
    const char * restrict format,
    …)
        _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vsnprintf(
    size_t n,
    char s[restrict static n],
    const char * restrict format,
    …)
        _Pre(s) _Pre(format)
        _Pre(n) _Pre(n <= STDC_VA_MBS_MAX)
        _Post((_ReturnValue < 0) || stdc_vismbs(n, s))
        ; // Additional runtime constraints apply
int stdc_vsprintf(
    size_t n,
    char s[restrict static n],
    const char * restrict format,
    …)
        _Pre(s) _Pre(format)
        _Pre(n) _Pre(n <= STDC_VA_MBS_MAX)
        _Post(stdc_vless(_ReturnValue, n))
        _Post((_ReturnValue < 0) || stdc_vismbs(n, s))
        ; // Additional runtime constraints apply
int stdc_vsscanf(
    const char * restrict s,
    const char * restrict format,
    …)
        _Pre(s) _Pre(format)
        ; // Additional runtime constraints apply

3.1.3 Format functions with va_list

int stdc_vfprintf(
    FILE * restrict stream,
    const char * restrict format,
    va_list arg)
        _Pre(stream) _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vfscanf(
    FILE * restrict stream,
    const char * restrict format,
    va_list arg)
        _Pre(stream) _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vprintf(
    const char * restrict format,
    va_list arg)
        _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vscanf(
    const char * restrict format,
    va_list arg)
        _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vsnprintf(
    size_t n,
    char s[restrict static n],
    const char * restrict format,
    va_list arg)
        _Pre(s) _Pre(format)
        _Pre(n) _Pre(n <= STDC_VA_MBS_MAX)
        _Post((_ReturnValue < 0) || stdc_vismbs(n, s))
        ; // Additional runtime constraints apply
int stdc_vsprintf(
    size_t n,
    char s[restrict static n],
    const char * restrict format,
    va_list arg)
        _Pre(s) _Pre(format)
        _Pre(n) _Pre(n <= STDC_VA_MBS_MAX)
        _Post(stdc_vless(_ReturnValue, n))
        _Post((_ReturnValue < 0) || stdc_vismbs(n, s))
        ; // Additional runtime constraints apply
int stdc_vsscanf(
    const char * restrict s,
    const char * restrict format,
    va_list arg)
        _Pre(s) _Pre(format)
        ; // Additional runtime constraints apply

3.1.4 String copying

char* stdc_strcpy(
    size_t dstmax,
    char dst[restrict static dstmax],
    const char src[restrict static 1])
        _Pre(dst) _Pre(src) _Pre(dstmax)
        _Pre(dstmax <= STDC_MBS_MAX)
        _Pre(size_t srclen  = stdc_strnlen(dstmax, src); srclen < dstmax)
        // srclen is less than STDC_MBS_MAX,
        // so the addition does not overflow
        _Pre(size_t srcmax  = srclen+1; true)
        _Pre(stdc_brange_check2(srcmax, dst, srcmax, src))
        _Post(!dst[srclen])
        _Post(_ReturnValue  == dst)
        [[unsequenced]];

char* stdc_strcat(
    size_t dstmax,
    char dst[restrict static dstmax],
    const char * restrict src)
        _Pre(dst) _Pre(src) _Pre(dstmax)
        _Pre(dstmax <= STDC_MBS_MAX)
        _Pre(size_t dstlen  = stdc_strnlen(dstmax, dst); dstlen < dstmax)
        _Pre(size_t srclen  = stdc_strnlen(dstmax, src); srclen < dstmax)
        // dstlen and srclen are less than STDC_MBS_MAX,
        // so the addition does not overflow
        _Pre(size_t rlen    = dstlen + srclen; rlen < dstmax)
        // rlen and srclen are less than STDC_MBS_MAX,
        // so the additions do not overflow
        _Pre(stdc_brange_check2(rlen+1, dst, srclen+1, src))
        _Post(!dst[rlen])
        _Post(_ReturnValue  == dst)
        [[unsequenced]];

char* stdc_strncat(
    size_t dstmax,
    char dst[restrict static dstmax],
    const char * restrict src,
    size_t n)
        _Pre(dst) _Pre(src) _Pre(dstmax)
        _Pre(dstmax <= STDC_MBS_MAX)
        _Pre(size_t dstlen  = stdc_strnlen(dstmax, dst); dstlen < dstmax)
        _Pre(size_t srclen  = stdc_strnlen(n, src); srclen < dstmax)
        // dstlen and srclen are less than STDC_MBS_MAX,
        // so the addition does not overflow
        _Pre(size_t rlen    = dstlen + srclen; rlen < dstmax)
        // rlen and srclen are less than STDC_MBS_MAX,
        // so the additions do not overflow
        _Pre(stdc_brange_check2(rlen+1, dst, stdc_min(srclen+1, n), src))
        _Post(!dst[rlen])
        _Post(_ReturnValue  == dst)
        [[unsequenced]];

Other than the Annex K counterpart strncpy_s, the function stdc_strncpy follows the definition of strncpy, that is, all trailing bytes, if any, are overwritten with zeroes.

char* stdc_strncpy(
    size_t dstmax,
    char dst[restrict static dstmax],
    const char src[restrict static 1],
    rsize_t n)
        _Pre(dst) _Pre(src) _Pre(dstmax)
        _Pre(dstmax <= STDC_MBS_MAX)
        _Pre(n <= dstmax)
        _Pre(size_t srclen  = stdc_strnlen(n, src); true)
        _Pre(stdc_brange_check2(n, dst, stdc_min(srclen+1, n), src))
        _Post(srclen    == n || !dst[srclen])
        _Post(_ReturnValue  == dst)
        [[unsequenced]];

3.1.5 Tokenization

Other than the existing functions strtok and strtok_s, stdc_strtok always expects that buf points to the (remaining) character array that is to be tokenized. The value of ptr[0] on entry to a call is ignored.

The argument delim is expected to be a ‘’short string’’ (null terminated!) of less than CHAR_MAX characters that contains a set of delimiter characters that are used to split up buf[] into tokens. The null character is always assumed to be part of that set of delimiter characters.

The procedure is the same as for strtok.

If after that there remains a part of the character array to be tokenized, ptr[0] is set to its start and buflenp[0] is set to its array length; if the whole array has been searched, ptr[0] is set to a null pointer and buflenp[0] is set to zero.

Note that other than strtok and strtok_s, stdc_strtok always requires that buf is non-null and points to the start of the array that is to be tokenized. No special case for a continuation of tokenization is needed, in particular the set of delimiter characters may vary from call to call. No state other than the pointed-to objects is needed for each call.

To tokenize an array iteratively the following scheme can be used

char* position  = myArray;
size_t len  = myArrayLen;
while (position) {
    char* token = stdc_strtok(&len, position, Delimiters, &position);
    if (!token) break;
    … use token …
}

The interface looks as follows

char *stdc_strtok(
    size_t buflenp[restrict static 1],
    char buf[restrict static buflenp[0]],
    const char delim[restrict static 1],
    char * ptr[restrict static 1])
        _Pre(buflenp) _Pre(buf) _Pre(delim) _Pre(ptr)
        _Pre(size_t buflen  = buflenp[0]; buflen <= STDC_MBS_MAX)
        _Pre(size_t delimlen    = stdc_strnlen(CHAR_MAX, delim); delimlen < CHAR_MAX)
        _Pre(stdc_brange_check4(
            sizeof(char[buflen]), buf,
            sizeof(char[delimlen+1]), delim,
            sizeof(size_t), buflenp,
            sizeof(char*), ptr))
        // postconditions
        _Post(buflenp[0] < buflen) // buflenp[0] always decreases
        _Post(!ptr[0]   == !buflenp[0]) // either both or none
        _Post(char* rempos  = buf + (buflen - buflenp[0]))
        _Post(_ReturnValue || (buf <= _ReturnValue))
        _Post(_ReturnValue || (_ReturnValue < rempos))
        // if !ptr[0], end was reached, otherwise
        _Post(!ptr[0] || _ReturnValue)
        _Post(!ptr[0] || (ptr[0]    == rempos))
        _Post(!ptr[0] || !_ReturnValue[-1]) // token is null terminated
        [[unsequenced]];

3.1.6 Copying entire arrays

void* stdc_memcpy(
    size_t dstmax,
    void dst[restrict static dstmax ? dstmax : 1],
    size_t n,
    const void src[restrict static n ? n : 1])
    _Pre(dst) _Pre(src)
    _Pre(dstmax <= STDC_MBS_MAX)
    _Pre(n <= STDC_MBS_MAX)
    _Pre(n <= dstmax)
    _Pre(!n || stdc_brange_check2(n, dst, n, src))
    _Post(_ReturnValue  == dst)
    [[unsequenced]];
void* stdc_memmove(
    size_t dstmax,
    void dst[restrict static dstmax ? dstmax : 1],
    size_t n,
    const void src[restrict static n ? n : 1])
    _Pre(dst) _Pre(src)
    _Pre(dstmax <= STDC_MBS_MAX)
    _Pre(n <= STDC_MBS_MAX)
    _Pre(n <= dstmax)
    _Post(_ReturnValue  == dst)
    [[unsequenced]];

3.2 Functions handling wide character strings

3.2.1 Functions used to express predicates

These are additional functions with possibly no equivalend in Annex K that are used to express predicates. They have the attribute [[unsequenced]] such that evaluation of checks can easily be moved around by an optimizing compiler.

3.2.1.1 The stdc_wcrange_check functions

These function check if the wide character arrays are mutually disjoint. For exampe for stdc_wcrange_check2 if a and b point to valid objects aObj and bObj, and if amax and bmax are not greater than sizeof(aObj) or sizeof(bObj), a call always has defined behavior.

bool stdc_wcrange_check2(
    size_t amax,
    wchar_t const a[static amax],
    size_t bmax,
    wchar_t const b[static bmax])
    _Pre(a) _Pre(b)
    [[unsequenced]];
bool stdc_wcrange_check3(
    size_t amax,
    wchar_t const a[static amax],
    size_t bmax,
    wchar_t const b[static bmax],
    size_t cmax,
    wchar_t const c[static cmax])
    _Pre(a) _Pre(b) _Pre(c)
    [[unsequenced]];
bool stdc_wcrange_check4(
    size_t amax,
    wchar_t const a[static amax],
    size_t bmax,
    wchar_t const b[static bmax],
    size_t cmax,
    wchar_t const c[static cmax],
    size_t dmax,
    wchar_t const d[static dmax])
    _Pre(a) _Pre(b) _Pre(c) _Pre(d)
    [[unsequenced]];

On implementations that have uintptr_t with the right properties, the body of stdc_wcrange_check2 could look as follows. This could easily be provided as an inline function, but would probably best be implemented as a builtin.

{
     return
         ((uintptr_t)(b + bmax) <= (uintptr_t)a)
         || ((uintptr_t)(a + amax) <= (uintptr_t)b);
}

3.2.1.2 The stdc_wcsnlen function

This function checks for the first position of a null wide character in the wide character array, if any. If s is a null pointer or points to a valid object Obj and if maxsize is not greater than sizeof(Obj) a call always has defined behavior.

size_t stdc_wcsnlen(
    size_t maxsize,
    const wchar_t *s)
        _Post(s || !_ReturnValue)
        _Post(_ReturnValue <= maxsize)
        _Post(!_ReturnValue || maxsize)
        _Post(_ReturnValue || !s || !maxsize || !s[0])
        _Post((_ReturnValue == maxsize) || !s[_ReturnValue])
        [[unsequenced]];

3.2.1.3 The stdc_iswcs function

This additional function checks if the wide character array is a valid string or not. If s is a null pointer or points to a valid object Obj and if maxsize is not greater than sizeof(Obj) a call always has defined behavior.

bool stdc_iswcs(
    size_t maxsize
    const wchar_t s[static maxsize ? maxsize : 1])
    [[unsequenced]];

The body of this function could look as follows. This could easily be provided as an inline function.

{
        if (!maxsize || !s) return false;
        else return !s[0] || (stdc_wcsnlen(maxsize, s) < maxsize);
}

3.2.2 Format functions with variable argument list

int stdc_vfwprintf(
    FILE * restrict stream,
    const wchar_t * restrict format,
    …)
        _Pre(stream) _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vfwscanf(
    FILE * restrict stream,
    const wchar_t * restrict format,
    …)
        _Pre(stream) _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vwprintf(
    const wchar_t * restrict format,
    …)
        _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vwscanf(
    const wchar_t * restrict format,
    …)
        _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vsnwprintf(
    size_t n,
    wchar_t s[restrict static n],
    const wchar_t * restrict format,
    …)
        _Pre(s) _Pre(format)
        _Pre(n) _Pre(n <= STDC_VA_MBS_MAX)
        _Post((_ReturnValue < 0) || stdc_v(n, s))
        ; // Additional runtime constraints apply
int stdc_vswprintf(
    size_t n,
    wchar_t s[restrict static n],
    const wchar_t * restrict format,
    …)
        _Pre(s) _Pre(format)
        _Pre(n) _Pre(n <= STDC_VA_MBS_MAX)
        _Post(stdc_v(_ReturnValue, n))
        _Post((_ReturnValue < 0) || stdc_v(n, s))
        ; // Additional runtime constraints apply
int stdc_vswscanf(
    const wchar_t * restrict s,
    const wchar_t * restrict format,
    …)
        _Pre(s) _Pre(format)
        ; // Additional runtime constraints apply

3.2.3 Format functions with va_list

int stdc_vfwprintf(
    FILE * restrict stream,
    const wchar_t * restrict format,
    va_list arg)
        _Pre(stream) _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vfwscanf(
    FILE * restrict stream,
    const wchar_t * restrict format,
    va_list arg)
        _Pre(stream) _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vwprintf(
    const wchar_t * restrict format,
    va_list arg)
        _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vwscanf(
    const wchar_t * restrict format,
    va_list arg)
        _Pre(format)
        ; // Additional runtime constraints apply
int stdc_vsnwprintf(
    size_t n,
    wchar_t s[restrict static n],
    const wchar_t * restrict format,
    va_list arg)
        _Pre(s) _Pre(format)
        _Pre(n) _Pre(n <= STDC_VA_MBS_MAX)
        _Post((_ReturnValue < 0) || stdc_v(n, s))
        ; // Additional runtime constraints apply
int stdc_vswprintf(
    size_t n,
    wchar_t s[restrict static n],
    const wchar_t * restrict format,
    va_list arg)
        _Pre(s) _Pre(format)
        _Pre(n) _Pre(n <= STDC_VA_MBS_MAX)
        _Post(stdc_v(_ReturnValue, n))
        _Post((_ReturnValue < 0) || stdc_v(n, s))
        ; // Additional runtime constraints apply
int stdc_vswscanf(
    const wchar_t * restrict s,
    const wchar_t * restrict format,
    va_list arg)
        _Pre(s) _Pre(format)
        ; // Additional runtime constraints apply

3.2.4 String copying

wchar_t* stdc_wcscpy(
    size_t dstmax,
    wchar_t dst[restrict static dstmax],
    const wchar_t src[restrict static 1])
        _Pre(dst) _Pre(src) _Pre(dstmax)
        _Pre(dstmax <= STDC_WCS_MAX)
        _Pre(size_t srclen  = stdc_wcsnlen(dstmax, src); srclen < dstmax)
        // srclen is less than STDC_WCS_MAX,
        // so the addition does not overflow
        _Pre(size_t srcmax  = srclen+1; true)
        _Pre(stdc_wcrange_check2(srcmax, dst, srcmax, src))
        _Post(!dst[srclen])
        _Post(_ReturnValue  == dst)
        [[unsequenced]];

wchar_t* stdc_wcscat(
    size_t dstmax,
    wchar_t dst[restrict static dstmax],
    const wchar_t * restrict src)
        _Pre(dst) _Pre(src) _Pre(dstmax)
        _Pre(dstmax <= STDC_WCS_MAX)
        _Pre(size_t dstlen  = stdc_wcsnlen(dstmax, dst); dstlen < dstmax)
        _Pre(size_t srclen  = stdc_wcsnlen(dstmax, src); srclen < dstmax)
        // dstlen and srclen are less than STDC_WCS_MAX,
        // so the addition does not overflow
        _Pre(size_t rlen    = dstlen + srclen; rlen < dstmax)
        // rlen and srclen are less than STDC_WCS_MAX,
        // so the additions do not overflow
        _Pre(stdc_wcrange_check2(rlen+1, dst, srclen+1, src))
        _Post(!dst[rlen])
        _Post(_ReturnValue  == dst)
        [[unsequenced]];

wchar_t* stdc_wcsncat(
    size_t dstmax,
    wchar_t dst[restrict static dstmax],
    const wchar_t * restrict src,
    size_t n)
        _Pre(dst) _Pre(src) _Pre(dstmax)
        _Pre(dstmax <= STDC_WCS_MAX)
        _Pre(size_t dstlen  = stdc_wcsnlen(dstmax, dst); dstlen < dstmax)
        _Pre(size_t srclen  = stdc_wcsnlen(n, src); srclen < dstmax)
        // dstlen and srclen are less than STDC_WCS_MAX,
        // so the addition does not overflow
        _Pre(size_t rlen    = dstlen + srclen; rlen < dstmax)
        // rlen and srclen are less than STDC_WCS_MAX,
        // so the additions do not overflow
        _Pre(stdc_wcrange_check2(rlen+1, dst, stdc_min(srclen+1, n), src))
        _Post(!dst[rlen])
        _Post(_ReturnValue  == dst)
        [[unsequenced]];

Other than the Annex K counterpart wcsncpy_s, the function stdc_wcsncpy follows the definition of wcsncpy, that is, all trailing wide characters, if any, are overwritten with zeroes.

wchar_t* stdc_wcsncpy(
    size_t dstmax,
    wchar_t dst[restrict static dstmax],
    const wchar_t src[restrict static 1],
    rsize_t n)
        _Pre(dst) _Pre(src) _Pre(dstmax)
        _Pre(dstmax <= STDC_WCS_MAX)
        _Pre(n <= dstmax)
        _Pre(size_t srclen  = stdc_wcsnlen(n, src); true)
        _Pre(stdc_wcrange_check2(n, dst, stdc_min(srclen+1, n), src))
        _Post(srclen    == n || !dst[srclen])
        _Post(_ReturnValue  == dst)
        [[unsequenced]];

3.2.5 Tokenization

Other than the existing functions wcstok and wcstok_s, stdc_wcstok always expects that buf points to the (remaining) wide character array that is to be tokenized. The value of ptr[0] on entry to a call is ignored.

The argument delim is expected to be a ‘’short wide string’’ (null terminated!) of less than WCHAR_MAX wide characters that contains a set of delimiter wide characters that are used to split up buf[] into tokens. The null wide character is always assumed to be part of that set of delimiter wide characters.

The procedure is the same as for wcstok.

If after that there remains a part of the wide character array to be tokenized, ptr[0] is set to its start and buflenp[0] is set to its array length; if the whole array has been searched, ptr[0] is set to a null pointer and buflenp[0] is set to zero.

Note that other than strtok and strtok_s, stdc_wcstok always requires that buf is non-null and points to the start of the array that is to be tokenized. No special case for a continuation of tokenization is needed, in particular the set of delimiter wide characters may vary from call to call. No state other than the pointed-to objects is needed for each call.

To tokenize an array iteratively the following scheme can be used

wchar_t* position   = myArray;
size_t len  = myArrayLen;
while (position) {
    wchar_t* token  = stdc_wcstok(&len, position, Delimiters, &position);
    if (!token) break;
    … use token …
}

The interface looks as follows

wchar_t *stdc_wcstok(
    size_t buflenp[restrict static 1],
    wchar_t buf[restrict static buflenp[0]],
    const wchar_t delim[restrict static 1],
    wchar_t * ptr[restrict static 1])
        _Pre(buflenp) _Pre(buf) _Pre(delim) _Pre(ptr)
        _Pre(size_t buflen  = buflenp[0]; buflen <= STDC_WCS_MAX)
        _Pre(size_t delimlen    = stdc_wcsnlen(WCHAR_MAX, delim); delimlen < WCHAR_MAX)
        _Pre(stdc_brange_check4(
            sizeof(wchar_t[buflen]), buf,
            sizeof(wchar_t[delimlen+1]), delim,
            sizeof(size_t), buflenp,
            sizeof(wchar_t*), ptr))
        // postconditions
        _Post(buflenp[0] < buflen) // buflenp[0] always decreases
        _Post(!ptr[0]   == !buflenp[0]) // either both or none
        _Post(wchar_t* rempos   = buf + (buflen - buflenp[0]))
        _Post(_ReturnValue || (buf <= _ReturnValue))
        _Post(_ReturnValue || (_ReturnValue < rempos))
        // if !ptr[0], end was reached, otherwise
        _Post(!ptr[0] || _ReturnValue)
        _Post(!ptr[0] || (ptr[0]    == rempos))
        _Post(!ptr[0] || !_ReturnValue[-1]) // token is null terminated
        [[unsequenced]];

3.2.6 Copying entire arrays

wchar_t* stdc_wmemcpy(
    size_t dstmax,
    wchar_t dst[restrict static dstmax ? dstmax : 1],
    size_t n,
    const wchar_t src[restrict static n ? n : 1])
    _Pre(dst) _Pre(src)
    _Pre(dstmax <= STDC_WCS_MAX)
    _Pre(n <= STDC_WCS_MAX)
    _Pre(n <= dstmax)
    _Pre(!n || stdc_wcrange_check2(n, dst, n, src))
    _Post(_ReturnValue  == dst)
    [[unsequenced]];
wchar_t* stdc_wmemmove(
    size_t dstmax,
    wchar_t dst[restrict static dstmax ? dstmax : 1],
    size_t n,
    const wchar_t src[restrict static n ? n : 1])
    _Pre(dst) _Pre(src)
    _Pre(dstmax <= STDC_WCS_MAX)
    _Pre(n <= STDC_WCS_MAX)
    _Pre(n <= dstmax)
    _Post(_ReturnValue  == dst)
    [[unsequenced]];

3.2.7 Stateless functions for string conversions

Some of the original C library functions have call variants that accept null pointer arguments to calculate a length. For these cases we provide two different function interfaces, one for the complete conversion task, and the other (with a len suffix) to just compute the length.

These functions all depend on locale, so they cannot be [[unsequenced]] or [[reproducible]].

int stdc_mb_dependent(void);

int stdc_mblen(
    size_t smax,
    char s[restrict static smax])
        _Pre(size_t mb_cur_max = MB_CUR_MAX; true)
        _Pre(s) _Pre(smax) _Pre(smax <= STDC_MBS_MAX)
        // If an encoding error occured the return value is -1
        _Post((_ReturnValue == -1) || (_ReturnValue > 0))
        _Post(_ReturnValue <= mb_cur_max);

int stdc_wctomblen(wchar_t wc)
        _Pre(size_t mb_cur_max = MB_CUR_MAX; true)
        // If an encoding error occured the return value is -1
        _Post((_ReturnValue == -1) || (_ReturnValue > 0))
        _Post(_ReturnValue <= mb_cur_max);

int stdc_wctomb(
    size_t dstmax,
    char dst[restrict static dstmax],
    wchar_t wc)
        _Pre(size_t mb_cur_max = MB_CUR_MAX; true)
        _Pre(dst) _Pre(dstmax) _Pre(dstmax <= STDC_MBS_MAX)
        // If an encoding error occured the return value is -1
        _Post((_ReturnValue == -1) || (_ReturnValue > 0))
        _Post(_ReturnValue <= stdc_min(dstmax, mb_cur_max));

size_t stdc_mbstowcslen(
    size_t srcmax,
    const char src[restrict static srcmax])
        _Pre(src) _Pre(srcmax) _Pre(srcmax <= STDC_MBS_MAX)
        // If an encoding error occured the return value is stdc_err_enc
        _Post((_ReturnValue == stdc_err_enc) || (_ReturnValue < STDC_WCS_MAX));

size_t stdc_mbstowcs(
    size_t dstmax,
    wchar_t dst[restrict static dstmax],
    size_t srcmax,
    const char src[restrict static srcmax])
        _Pre(src) _Pre(srcmax) _Pre(srcmax <= STDC_MBS_MAX)
        _Pre(dst) _Pre(dstmax) _Pre(dstmax <= STDC_WCS_MAX)
        _Pre(size_t srclen = stdc_strnlen(srcmax, src); true)
        _Pre(stdc_brange_check2(sizeof(wchar_t[dstmax]), dst, stdc_min(srclen+1, srcmax), src))
        // If an encoding error occured the return value is stdc_err_enc
        _Post((_ReturnValue == stdc_err_enc) || (_ReturnValue <= dstmax))
        // If possible, the destination is a wide string
        _Post((_ReturnValue != stdc_err_enc) || !dst[0])
        _Post((_ReturnValue == stdc_err_enc) || !dst[_ReturnValue])
        // The last wide character, if any, in the destination is not a null character
        _Post((_ReturnValue == stdc_err_enc) || (_ReturnValue > 0) || dst[_ReturnValue-1]);

size_t stdc_wcstombs(
    size_t dstmax,
    char dst[restrict static dstmax],
    size_t srcmax,
    const wchar_t src[restrict static srcmax])
        _Pre(dst) _Pre(dstmax) _Pre(dstmax <= STDC_MBS_MAX)
        _Pre(src) _Pre(srcmax) _Pre(srcmax <= STDC_WCS_MAX)
        _Pre(size_t srclen = stdc_wcsnlen(srcmax, src); true)
        _Pre(stdc_brange_check2(dstmax, dst, sizeof(wchar_t[stdc_min(srclen+1, srcmax)]), src))
        // If an encoding error occured the return value is stdc_err_enc
        _Post((_ReturnValue == stdc_err_enc) || (_ReturnValue <= dstmax));

3.2.8 Restartable functions for string conversions

These functions additionally store a conversion state in a parameter of type mbstate_t[1]. Where possible, the rather complicated C library interfaces of subclause 7.33.6.4 are split according to the different case that occur in the descriptions, there. In particular, for 7.33.6.4 functions that accept a nullptr instead of a pointer into a destination array, we provide interfaces with the suffix len that compute the corresponding (wide) string length that a destination would have; these functions receive a const qualified mbstate_t parameter and internally work on a copy of that state.

These functions all depend on locale, so they cannot be [[unsequenced]] or [[reproducible]].

size_t stdc_mbsreset(mbstate_t ps[restrict static 1])
        _Post(_ReturnValue <= mb_cur_max);

size_t stdc_mbrtowclen(
    size_t srcmax,
    char const src[restrict static srcmax],
    mbstate_t const ps[restrict static 1])
        _Pre(src) _Pre(srcmax) _Pre(srcmax <= STDC_MBS_MAX)
        // If an encoding error occured the return value is stdc_err_enc
        _Post((_ReturnValue != stdc_err_enc) || (errno == EILSEQ))
        // If the mb character is incomplete the return value is stdc_err_incomp
        _Post((_ReturnValue >= stdc_err_incomp) || (_ReturnValue <= srcmax));

size_t stdc_mbrtowc(
    wchar_t dst[restrict static 1],
    size_t srcmax,
    char const src[restrict static srcmax],
    mbstate_t ps[restrict static 1])
        _Pre(dst)
        _Pre(src) _Pre(srcmax) _Pre(srcmax <= STDC_MBS_MAX)
        // If an encoding error occured the return value is stdc_err_enc
        _Post((_ReturnValue != stdc_err_enc) || (errno == EILSEQ))
        // If the mb character is incomplete the return value is stdc_err_incomp
        _Post((_ReturnValue >= stdc_err_incomp) || (_ReturnValue <= srcmax))
        _Post((_ReturnValue >= stdc_err_incomp) || _ReturnValue || !dst[0]);

size_t stdc_wcrtomblen(
    wchar_t wc,
    mbstate_t const ps[restrict static 1])
        _Pre(size_t mb_cur_max = MB_CUR_MAX; true)
        _Pre(ps)
        // If an encoding error occured the return value is stdc_err_enc
        _Post(_ReturnValue);
        _Post((_ReturnValue == stdc_err_enc) || (_ReturnValue <= mb_cur_max));
        _Post(wc || (_ReturnValue <= mb_cur_max));

size_t stdc_wcrtomb(
    size_t dstmax,
    char dst[restrict static dstmax],
    wchar_t wc,
    mbstate_t ps[restrict static 1])
        _Pre(size_t mb_cur_max = MB_CUR_MAX; true)
        _Pre(dst) _Pre(dstmax >= mb_cur_max) _Pre(dstmax <= STDC_MBS_MAX)
        _Pre(ps)
        // If an encoding error occured the return value is stdc_err_enc
        _Post(_ReturnValue);
        _Post((_ReturnValue == stdc_err_enc) || (_ReturnValue <= mb_cur_max));
        _Post(wc || (_ReturnValue <= mb_cur_max))
        _Post(wc || !dst[_ReturnValue]);

size_t stdc_mbsrtowcslen(
    size_t srcmax,
    const char src[restrict static srcmax],
    mbstate_t const ps[restrict static 1])
        _Pre(src) _Pre(srcmax) _Pre(srcmax <= STDC_MBS_MAX)
        // If an encoding error occured the return value is stdc_err_enc
        _Post((_ReturnValue != stdc_err_enc) || (errno == EILSEQ))
        _Post((_ReturnValue == stdc_err_enc) || (_ReturnValue <= STDC_WCS_MAX));

size_t stdc_mbsrtowcs(
    size_t dstmax,
    wchar_t dst[restrict static dstmax],
    size_t srcmax,
    const char src[restrict static srcmax],
    const char* srcp[restrict static 1],
    mbstate_t ps[restrict static 1])
        _Pre(dst) _Pre(dstmax) _Pre(dstmax <= STDC_WCS_MAX)
        _Pre(src) _Pre(srcmax) _Pre(srcmax <= STDC_MBS_MAX)
        // If an encoding error occured the return value is stdc_err_enc
        _Post((_ReturnValue != stdc_err_enc) || (errno == EILSEQ))
        _Post((_ReturnValue == stdc_err_enc) || (_ReturnValue <= dstmax))
        _Post((_ReturnValue == stdc_err_enc) || (srcp[0] <= (src + srcmax)));

size_t stdc_wcsrtombslen(
    size_t srcmax,
    const wchar_t src[restrict static srcmax],
    mbstate_t const ps[restrict static 1])
        _Pre(src) _Pre(srcmax) _Pre(srcmax <= STDC_WCS_MAX)
        // If an encoding error occured the return value is stdc_err_enc
        _Post((_ReturnValue != stdc_err_enc) || (errno == EILSEQ))
        _Post((_ReturnValue == stdc_err_enc) || (_ReturnValue <= STDC_MBS_MAX));

size_t stdc_wcsrtombs(
    size_t dstmax,
    char dst[restrict static dstmax],
    size_t srcmax,
    const wchar_t src[restrict static srcmax],
    const wchar_t* srcp[restrict static 1],
    mbstate_t ps[restrict static 1])
        _Pre(dst) _Pre(dstmax) _Pre(dstmax <= STDC_MBS_MAX)
        _Pre(src) _Pre(srcmax) _Pre(srcmax <= STDC_WCS_MAX)
        // If an encoding error occured the return value is stdc_err_enc
        _Post((_ReturnValue != stdc_err_enc) || (errno == EILSEQ))
        _Post((_ReturnValue == stdc_err_enc) || (_ReturnValue <= dstmax))
        // If srcp[0] is null, the end of the source string had been reached.
        // Otherwise, srcp[0] shows the progress inside the source string.
        _Post((_ReturnValue == stdc_err_enc) || srcp[0] || (src < srcp[0]))
        _Post((_ReturnValue == stdc_err_enc) || srcp[0] || (srcp[0] <= (src + srcmax)));

3.3 Misc

char* stdc_tmpnam(char s[static L_tmpnam])
        _Pre(s)
        _Post(!_ReturnValue || (_ReturnValue == s));
        _Post(!_ReturnValue || stdc_ismbs(L_tmpnam, s));

FILE * stdc_fopen(
    const char filename[restrict static 1],
    const char mode[restrict static 1])
        _Pre(filename) _Pre(stdc_ismbs(FILENAME_MAX, filename))
        _Pre(mode)
        _Pre(size_t modelen = stdc_strnlen(6, mode); modelen ∧ (modelen < 6))
        _Pre((strspn(mode, "rwa") ≡ 1))
        _Pre(strspn(mode+1, "bxp+") ≡ (modelen-1));

// Change the mode of the opened stream
inline _Contracts(FILE *, stdc_fremode, mode, stream)(
    const char mode[restrict static 1],
    FILE * restrict stream)
        _Pre(!filename || stdc_ismbs(FILENAME_MAX, filename))
        _Pre(mode) _Pre(stdc_ismbs(6, mode))
        _Pre(stream)
        _Pre(mode)
        _Pre(size_t modelen = stdc_strnlen(6, mode); modelen ∧ (modelen < 6))
        _Pre(strspn(mode, "rwa") ≡ 1)
        _Pre(strspn(mode+1, "bxp+") ≡ (modelen-1))
        _Post(!_ReturnValue || (_ReturnValue == stream));


FILE * stdc_freopen(
    const char* filename,
    const char mode[restrict static 1],
    FILE * restrict stream)
        _Pre(!filename || stdc_ismbs(FILENAME_MAX, filename))
        _Pre(mode) _Pre(stdc_ismbs(6, mode))
        _Pre(stream)
        _Pre(mode)
        _Pre(size_t modelen = stdc_strnlen(6, mode); modelen ∧ (modelen < 6))
        _Pre(strspn(mode, "rwa") ≡ 1)
        _Pre(strspn(mode+1, "bxp+") ≡ (modelen-1))
        _Post(!_ReturnValue || (_ReturnValue == stream));

size_t stdc_getenvlen(const char name[restrict static 1])
        _Pre(name) _Pre(stdc_ismbs(STDC_MBS_MAX, name))
        // returns stdc_err_notf if name is not found
        _Post((_ReturnValue == stdc_err_notf) || (_ReturnValue <= STDC_MBS_MAX));

size_t stdc_getenv(
    size_t valuemax,
    char value[restrict static valuemax],
    const char name[restrict static 1]
    )
        _Pre(name) _Pre(stdc_ismbs(STDC_MBS_MAX, name))
        _Pre(valuemax) _Pre(valuemax <= STDC_MBS_MAX)
        // Under all circumstances value is made a string.
        // returns stdc_err_notf if name is not found
        _Post((_ReturnValue == stdc_err_notf) || !value[0])
        // If valuemax is too small to store the result string,
        // it is truncated.
        _Post((_ReturnValue == stdc_err_notf) || !value[stdc_min(valuemax, _ReturnValue)]);

QVoid *stdc_bsearch(
    size_t size,
    const void key[static size],
    size_t nmemb,
    QVoid base[static nmemb][size],
    int (*compar)(
        const void *k,
        const void *y,
        size_t contextmax,
        void context[restrict static contextmax])
        [[unsequenced]],
    size_t contextmax,
    void context[restrict static contextmax])
        _Pre(key) _Pre(size) _Pre(size <= STDC_MBS_MAX)
        _Pre(base) _Pre(nmemb) _Pre(nmemb <= STDC_MBS_MAX/size)
        _Pre(compar)
        _Pre(!context || (contextmax && (contextmax <= STDC_MBS_MAX)))
        _Post(!_ReturnValue || !compar(key, _ReturnValue, contextmax, context))
        [[unsequenced]];

// Check if the array is already ordered.
bool stdc_qsort_check(
    size_t size,
    size_t nmemb,
    void base[static nmemb][size],
    int (*compar)(
        const void *x,
        const void *y,
        size_t contextmax,
        void context[restrict static contextmax])
        [[unsequenced]],
    size_t contextmax,
    void context[restrict static contextmax])
        _Pre(size) _Pre(size <= STDC_MBS_MAX)
        _Pre(base) _Pre(nmemb) _Pre(nmemb <= STDC_MBS_MAX/size)
        _Pre(compar)
        _Pre(!context || (contextmax && (contextmax <= STDC_MBS_MAX)))
        [[unsequenced]];

void stdc_swap(
  size_t size,
  void a[static size],
  void b[static size])
    _Pre(size) _Pre(size <= STDC_MBS_MAX)
    _Pre(a) _Pre(b)
    [[unsequenced]];


void stdc_qsort(
    size_t size,
    size_t nmemb,
    void base[static nmemb][size],
    int (*compar)(
        const void *x,
        const void *y,
        size_t contextmax,
        void context[restrict static contextmax])
        [[unsequenced]],
    size_t contextmax,
    void context[restrict static contextmax])
        _Pre(size) _Pre(size <= STDC_MBS_MAX)
        _Pre(base) _Pre(nmemb) _Pre(nmemb <= STDC_MBS_MAX/size)
        _Pre(compar)
        _Pre(!context || (contextmax && (contextmax <= STDC_MBS_MAX)))
        _Post(stdc_qsort_check(size, nmemb, base, compar, contextmax, context))
        [[unsequenced]];


void* stdc_memset(
    size_t smax,
    void s[static smax],
    int c,
    size_t n)
        _Pre(s) _Pre(smax) _Pre(smax <= STDC_MBS_MAX)
        _Pre(!((unsigned)c >> CHAR_BIT))
        _Post(_ReturnValue == s)
        [[unsequenced]];

size_t stdc_strerrorlen(int errnum)
        _Post(_ReturnValue)
        _Post(_ReturnValue <= STDC_MBS_MAX);

size_t stdc_strerror(
    size_t bufmax,
    void buf[static bufmax],
    int errnum)
        _Pre(buf) _Pre(bufmax) _Pre(bufmax <= STDC_MBS_MAX)
        _Post(_ReturnValue)
        _Post(_ReturnValue <= STDC_MBS_MAX)
        // The buffer always holds a string
        // Applies the truncation rules of strerror_s
        _Post((_ReturnValue >= bufmax) || !buf[_ReturnValue]);
        _Post((_ReturnValue < bufmax) || !buf[bufmax-1])
        _Post((_ReturnValue < bufmax) || (bufmax > 3) || (buf[bufmax-2] == '.'))
        _Post((_ReturnValue < bufmax) || (bufmax > 3) || (buf[bufmax-3] == '.'))
        _Post((_ReturnValue < bufmax) || (bufmax > 3) || (buf[bufmax-4] == '.'));

char* stdc_fgets(
    size_t n,
    char s[static n],
    FILE* stream)
        _Pre(n) _Pre(n <= STDC_MBS_MAX)
        _Pre(s)
        _Pre(stream)
        _Post(!_ReturnValue || (_ReturnValue == s))
        _Post(!_ReturnValue || stdc_ismbs(n, s))
        _Post(_ReturnValue || !s[0]);

char* stdc_asctime(
    const struct tm timeptr[static 1],
    char s[static 26])
        _Pre(s) _Pre(timeptr)
        _Pre(timptr->tm_year >= -1900)
        _Pre(timptr->tm_year <= 8099)
        _Post(!_ReturnValue || (_ReturnValue == s))
        _Post(!_ReturnValue || (s[3] == ' '))
        _Post(!_ReturnValue || (s[7] == ' '))
        _Post(!_ReturnValue || (s[10] == ' '))
        _Post(!_ReturnValue || (s[19] == ' '))
        _Post(!_ReturnValue || (s[24] == '\n'))
        _Post(!_ReturnValue || !s[25])
        [[unsequenced]];

char* stdc_ctime(
    const time_t timer,
    char s[static 26])
        _Pre(s)
        _Post(!_ReturnValue || (_ReturnValue == s))
        _Post(!_ReturnValue || (s[3] == ' '))
        _Post(!_ReturnValue || (s[7] == ' '))
        _Post(!_ReturnValue || (s[10] == ' '))
        _Post(!_ReturnValue || (s[19] == ' '))
        _Post(!_ReturnValue || (s[24] == '\n'))
        _Post(!_ReturnValue || !s[25])
        ; // locale dependent

struct tm *stdc_gmtime(
    const time_t timer,
    struct tm result[restrict static 1])
        _Pre(timer) _Pre(result)
        _Post(!_ReturnValue || (_ReturnValue == result))
        [[unsequenced]];

struct tm *stdc_localtime(
    const time_t timer,
    struct tm result[restrict static 1])
        _Pre(result)
        _Post(!_ReturnValue || (_ReturnValue == result))
        ; // locale dependent

Acknowledgments

Thanks to Robert Seacord for review and discussions.