Appendix B - Type system of eCv

The type system of eCv is based on C, with these changes:

The type 'pointer to array of T' is distinct from 'pointer to T'. The syntax 'T*' means 'pointer to T'. To specify 'pointer to array of T', use 'T* array'. You may not apply indexing or pointer arithmetic to non-array pointers.
Pointers (including pointers to arrays) are not nullable by default (i.e. zero is not an allowed value). You can specify that null is an allowed value using the type qualifier 'null', e.g. 'T* null' or 'T* array null'. The order of qualifiers 'array' and 'null' (and any other type qualifiers you use) is not significant. There is an implicit type conversion from each plain pointer type to the corresponding nullable pointer type, but not the other way round. To convert the other way, use 'not_null(e)' which asserts that e is not null and converts its type from 'T* null' to 'T*', or from 'T* array null' to 'T* array'.
Union types have an additional ghost field called the discriminant, which remembers the name of field the union was last assigned through. This field cannot be referred to at run-time (because it isn't stored), however it can be referred to in specifications via the holds operator. You may only access a union member if it was most recently assigned via the same member.
bool is a separate type
char is a separate type, not an alias for signed char or unsigned char
wchar_t is a separate type, not an alias for some other integral type
Each enumeration declaration creates a distinct type, not an alias for an integral type

Semantic differences between eCv and C90

The type of a string literal in eCv is const char* array (like C++ with the addition of array) instead of char*. Therefore, you cannot provide a string literal in a context where a value of type char* is required. This difference is backwards-compatible in the sense that any legal use of a string literal in eCv is also a legal use in C and has the same semantics.
The type of a wide string literal is const wchar_t * array instead of wchar_t *.
The type of a character literal in eCv is char (like C++) instead of int. If you want to use a character literal in a situation where a value of type int is required, you must cast it explicitly to type int. This change is backwards-compatible in that any legal use of a character literal in eCv is also a legal use in C, although some compilers might generate a warning that an explicit cast of a character literal to type int is redundant. You can define a char-literal-to-int conversion macro to avoid any such warnings. Note that in eCv it is illegal to use a character literal as the operand of sizeof, because this would yield a different result from C.

TOC