TOC
A ghost type, function or field is one that you can refer to in specifications, but not in code. As well as the predefined ones that eCv provides, you can declare your own ghost types, variables, functions and fucntion parameters, and you can declare ghost fields of your own struct and union types.
The predefined ghost fields of pointers and array pointers are read-only. Even though ghost fields are not stored at run-time, eCv can track their values and reason about them.
| Variable name and type | Description | Where declared |
| _ecv_seq<_ecv_VolatileBase> _ecv_vol_ops | Records the sequence of reads from and writes to volatile variables performed by the program | Built in |
Where these functions have names not beginning with _ecv_, they are declared as macros in the header files indicated, in terms of intrinsic functions whose names begin with _ecv_. You can therefore rename any whose names clash with your own identifiers.
| Function name and signature | Description | Where declared |
| bool _ecv_isNullTerminated(const char * array str) | Yields true if there is a null in str with an index between zero and the upper bound of str. Typically used in function preconditions to state that a parameter of type char* array or const char* array must be a null-terminated string. | Built in |
| bool _ecv_allBytesAre(const void* array p, int val, size_t num) | Yields true if the first n characters of memory addressed by p have the value val. Used to describe the semantics of memset and similar functions. | Built in |
| bool _ecv_equalBytes(const void* array p, const void* array q, size_t num) | Yields true if the first n characters of memory addressed by p and q are correspondingly equal. Used to describe the semantics of memcpy and similar functions. | Built in |
| template<typename T> T _ecv_readVolatile(T* p) writes(_ecv_vol_ops) | Read from the volatile variable at *p, record the read in _ecv_vol_ops and return the value read. | Built in |
| template<typename T> T _ecv_writeVolatile(T* p, T val) writes(_ecv_vol_ops) | Write val to the volatile variable at *p, record the write in _ecv_vol_ops and return val. | Built in |
Each array pointer type T* array (where T is any type) has the following ghost fields:
| Field name | Type | Description |
| all | T[ ] | All the elements of the array that is pointed to, including elements with a negative index (if any). If ap is an array pointer, then ap.all is a bit like *ap except that it returns the value of the whole array, instead of just the value of the array element that ap points to. Important: if you write a function postcondition involving a.all where a is a function parameter with array pointer type, then the postcondition is required to apply to the whole array including any negative indices. If the code of your function does not take account of possible negative indices, then the postcondition is likely to be unprovable. You can get round this by specifying that a is a pointer to the start of an array (so that there are never any negative indices), for example by including a.lwb == 0 in the function precondition. |
| base | T* array | A pointer to the same array re-based to point to its first element (so that offset is zero). You can test whether two array pointers a and b point into the same array using the expression a.base == b.base. |
| count | integer | The count of all elements in the array, equal to offset + lim. |
| indices | seq<integer> | The sequence lwb..upb, i.e. a sequence comprising all the valid indices of the array pointer. |
| lim | integer | One greater than the highest valid index. For any array pointer that was not created by pointer arithmetic, this is the number of elements in the array. Never less than zero. |
| lwb | integer | The lowest valid index, equal to (-offset). |
| offset | integer | The offset of the pointer into the array relative to the start of the array, as a number of elements. Zero for any array pointer that was not created by pointer arithmetic. Always between zero and count inclusive. |
| upb | integer | The highest valid index, equal to lim - 1. Never less than -1. |
The void pointer type void* has the following ghost fields:
| Field name | Type | Description |
| all | Universal object type | The object that the original pointer pointed to, or the whole array that the original array pointer pointed into, before it was converted to a void*. |
| lim | integer | The size of the object in characters, not including any part of it that has a negative offset from the pointer. If pv has type void* then ((char*)pv).lim == pv.lim. Never less than zero. |
| offset | integer | The offset of the pointer into the object relative to the start of the object, as a number of characters. Zero for any void* pointer that was obtained by converting a non-array pointer or a pointer to the start of an array. |
Each array type T [ ] (where T is any type) has the following ghost fields:
| Field name | Type | Description |
| count | integer | The count of elements, i.e. the same value as lim. |
| indices | seq<integer> | The sequence 0..upb, i.e. a sequence comprising all the valid indices of the array pointer. |
| lim | integer | One greater than the highest valid index, i.e. the number of elements in the array. |
| lwb | integer | The lowest valid index. Always zero. |
| upb | integer | The highest valid index, equal to lim - 1. |
Each array type T [ ] or sequence type seq<T> (where T is any type) has the following ghost member functions:
| Function name | Preconditions | Description of return value |
| seq<T> drop(integer n) | 0 <= n; n <= lim | A sequence comprising the array elements with the first n removed |
| bool isndec() | Element type T is a comparable type | true if and only if the elements are in nondecreasing order |
| bool isninc() | Element type T is a comparable type | true if and only if the elements are in nonincreasing order |
| T max() | Element type T is a comparable type; lim != 0 | The maximum element |
| T min() | Element type T is a comparable type; lim != 0 | The minimum element |
| seq<T> permndec() | Element type T is a comparable type | A sequence comprising the elements of the array sorted into nondecreasing order |
| seq<T> permninc() | Element type T is a comparable type | A sequence comprising the elements of the array sorted into nonincreasing order |
| seq<T> rev() | A sequence comprising the elements of the array in reverse order | |
| seq<T> slice(integer start, integer len) | 0 <= start; 0 <= len; start + len <= lim | A sequence comprising len elements from the array starting at index start. Equivalent to drop(start).take(len) |
| seq<T> take(integer n) | 0 <= n; n <= count | A sequence comprising the first n elements of the array |
Other ghost members of array and sequence types are available, as detailed in the Library Reference section of the Perfect Developer Language Reference Manual (look up class seq of X).
eCv Manual, Version 7.01, April 2017.
© 2017 Escher Technologies Limited. All rights reserved.