TOC
You can configure eCv to assume source code is C90, C99, C++ 1998 or C++ 2011. The choice is made in the compiler configuration dialog in the Project Manager, or using the -gl option if you are running eCv from the command line.
The following describes the core C90 language subset supported by eCv, in particular the restrictions placed on C constructs. Where these restrictions have equivalent or related MISRA-C 2004 rules, we quote the rule numbers.
Not all of the restrictions are rigidly enforced; some will give rise to warning (rather than error) messages if they are violated, allowing analysis to continue.
For information on constructs from C99 and C++ that eCv supports when you select on of those languages, see Appendix E.
eCv treats some additional words as keywords. These words may not be used as identifiers. Here is a list of them:
Normal keyword Underlying keyword Where used See section any _ecv_any 'any' expression Collections array _ecv_array Indicates that a pointer refers to an array array assert _ecv_assert Assertion statement assert assume _ecv_assume Assume declaration assume bool Boolean type Boolean types decrease _ecv_decrease Declares a loop variant decrease exists _ecv_exists 'exists' expression Quantified expressions false
Boolean false value Boolean types forall _ecv_forall 'forall' expression Quantified expressions ghost _ecv_ghost Declares that a declaration is for use in specifications only ghost (see also Ghosts) holds _ecv_holds 'holds' expression Disjoint expressions idiv _ecv_idiv An integer division operator that always rounds down Binary operators imod _ecv_imod An integer modulus operator that always yields a non-negative result Binary operators in _ecv_in Element-in-collecton operator Binary operators integer _ecv_integer Unbounded integer type ghost _ecv_interrupt Function specifier to indicate that the function is an interrupt service routine (to be added) invariant _ecv_invariant Declares a structure invariant invariant keep _ecv_keep Declares a loop invariant keep let _ecv_let Names a subexpression so you can refer to it in a larger expression let maxof _ecv_maxof Yields the maximum value in a type Type operators minof _ecv_minof Yields the minimum value in a type Type operators min_sizeof _ecv_minof Yields the minimum value that sizeof could yield for the same type Type operators not_null _ecv_not_null Cast a nullable pointer to a non-nullable pointer not_null null _ecv_null Declares that a pointer is nullable Nullable and non-nullable pointers _ecv_nullptr Null pointer literal Additional eCv++ keywords old _ecv_old Selects the original value of an expression instead of the final or current value in a postcondition, loop invariant or loop variant old out _ecv_out Indicates that a pointer parameter is used only to pass a value back to the caller Pointers as function parameters over _ecv_over 'over' expression Collections pass _ecv_pass Null statement pass post _ecv_post Declares a postcondition post _ecv_pow Exponentiation operator Binary operators pre _ecv_pre Declares a precondition pre result _ecv_result Refers to function result in a postcondition post returns _ecv_returns Declares a function return value returns some _ecv_some Indicates any object(s) of a specified type spec _ecv_spec Declares that a function prototype overrides another similar one that _ecv_that 'that' expression Collections those _ecv_those 'those' expression Collections true Boolean true value Boolean types wchar_t Wide character type below writes _ecv_writes Declares nonlocal variables that a function writes to writes value _ecv_value Refers to the value of the structure in a structure invariant, similar to (*this) in C++ yield _ecv_yield 'for..yield' and 'for..those..yield' expressions Collections zero_init _ecv_zero_init Yields the value of a type obtained by setting all bits to zero Type operators
If you must use one of the keywords in the above table as an identifier in your
program (perhaps because a third-party library header file uses it)
then there is a workaround. Apart from bool, false,
true and wchar_t, all the reserved words not beginning with _ecv_ are
defined in file ecv.h as macros equivalent to the
corresponding _ecv_ versions. After you #include "ecv.h"
at the start of your program, you may #undef
the keyword. So if you need to use e.g. result
as an identifier, you can #undef result, and then subsequently use
_ecv_result instead of result in eCv specifications.
Note: if you use keywords beginning with _ecv_ directly, then this may result in the column numbers in eCv error, warning and informational messages being incorrect (see later in this chapter).
eCv also places a number of identifiers beginning with _ecv_ in the global namespace, therefore you should not use identifiers beginning with _ecv_ in your source code.
Although we have listed wchar_t as a reserved word, if your source code is C90 or C99 (not C++) then you are allowed to use a typedef in a standard header file to define wchar_t with its usual meaning, i.e. the type of a wide character literal.If you are using any of the keywords {bool, true, false} to define your own Boolean type, you should make your own definitions conditional - see here.
eCv places the following restrictions on using of the C language.
eCv treats ":-" as a single token, rather than the two tokens ":" and "-". This means that conditional expressions such as the following, will not be parsed correctly:
c ? e :-f
c ? e :--x
The fix is simple: ensure that there is at least one space between the colon and the minus-sign, as in the following:
c ? e : -f
c ? e : --f
static or extern
variables/functions with short names that you may also want to use as parameter names.sizeof. int). (MISRA 8.2) struct Foo *
then type Foo must be defined somewhere. If necessary, declare a dummy definition, like this: #ifdef __ECV__
struct Foo { int x; }
#endif switch(i) {
case 1: /* ok */
case 2: /* ok */
...
break;
{
case 3: /* error, case label is inside another statement */
default: /* error, case label is inside another statement */
...
break;
}
case 4: { /* ok */
...
break;
}
}
switch(i) {
int temp1;
/* error, declarations not allowed here */
case 1: {
int temp2; /* ok, declaration is inside a compound statement */
...
}
break;
default:
int temp3; /* error, declarations not allowed here even in C99 or C++ mode */
...
break;
}
goto statement, the destination label must be later in the preprocessed source file that the goto keyword,
and must be in the same block as the goto keyword or in an enclosing block.
So backwards jumps and jumps into blocks are not permitted.
When processing C'99 or C++ source, a goto statement may not jump over any declarations that are in the same block as the destination label.C90 does not provide a Boolean type. C99 provides a boolean type called _Bool, and if you #include "stdbool.h" then it is also called bool and the corresponding literals are called false and true. C++ provides a Boolean type, calling it bool and the corresponding literals false and true.
eCv follows the C++ standard in order to provide stronger typing than C90. Therefore, in order that you can use the Boolean type in your code in a manner that your compiler will accept, you should do one of the following:
(a) Add the following to your standard header:
#if !defined(__ECV__) && !defined(__cplusplus)
/* we're neither running under eCv nor compiling as C++, so we need to define the Boolean type */
#if defined(__STDC_VERSION__) && (__STDC_VERSION__ >= 199901L)
/* we're compiling as C99 so use the definition in stdbool.h */
#include <stdbool.h>
#else
/* compiling as an older version of C */
/* define the Boolean type ourselves in a manner compatible with C99 and C++ */
typedef enum { false = 0, true = 1 } bool;
#endif
#endif
and then use the names bool, false and true in your code.
(b) If you are already using some names other than {bool, false, true}
to denote Boolean types and values, then do something like the following (this example assumes that you are using BOOL_T, FALSE and TRUE):
#if defined(__ECV__)
typedef bool BOOL_T;
#define FALSE (false)
#define TRUE (true)
#else
/* insert your own code here, e.g. the following */
/* typedef enum { FALSE = 0, TRUE = 1 } BOOL_T; */
#endif Pointers in C and C++ can be troublesome in several ways:
By default, eCv assumes when you declare a variable, parameter or function return value as having a pointer type, the value zero (or NULL) is not allowed. If you wish to allow this value, you must say so by using the null qualifier in the declaration. Here's an example:
void foo(int * p, int * null q) { ... }
...
int a = 1;
foo(NULL, &a); /* error, parameter p of foo() is not nullable */
foo(&a, NULL); /* ok, parameter q was declared nullable */
void copyError(const char * array msg, char * array dst, int dstSize)
{ ... }
The presence of the array keyword tells eCv that the msg and dst parameters point to arrays rather than single values. If you leave it out, then eCv will not allow you to perform indexing or any other sort of pointer arithmetic on those parameters. When you compile the code, array becomes a macro with an empty expansion, so your standard C or C++ compiler doesn’t notice it.
In this example, we’ve passed the size of the destination buffer in a separate int parameter, so that the code can limit how many characters it writes. However, in writing specifications, we often need to talk about the size of the array that a pointer points to even when we don’t have it available in a separate parameter. eCv treats an array pointer like a struct comprising three values: the pointer itself, the lower bound (i.e. index of the first element), and the limit (i.e. one plus the index of the last element). To refer to the lower bound or limit of dst we use the syntax dst.lwb or dst.lim respectively. We also allow dst.upb (for upper bound), which is defined as (dst.lim – 1). Of course, you cannot refer to these fields in code, but you can use them in specification constructs (such as preconditions, invariants, assertions) as much as you like. We call them ghost fields because they aren’t stored.
For example, let’s specify that when the copyError function is called, it assumes that dst points to an array with at least dstsize elements available. Here’s how we can specify that:
void copyError(const char * array msg, char * array dst, int dstSize)
pre(dst.lim >= dstSize)
{ ... }
An array pointer in C/C++ may only address the first element of an array, or one-past-the-last element, or any element in between. If p addresses the first element of an array of N elements, then p.lwb == 0 and p.lim == N. If it addresses one-past-the-last element, then p.lwb = -N and p.lim = 0. So p has implicit invariant p.lwb <= 0 && p.lim >= 0.
Within the body of copyError, eCv will attempt to prove that all accesses to msg and dst are in bounds. For example, the expression dst[i] has precondition dst.lwb <= i && i < dst.lim. Also, wherever copyError is called, eCv will attempt to prove that the precondition holds. So anywhere that buffer overflow is possible, there will be a corresponding a failed proof. If all the proofs succeed, and provided that no function with a precondition is ever called by external unproven code, we know that buffer overflow will not occur.
As with plain pointers, eCv assumes that array pointers may not take the value zero (i.e. NULL) unless you qualify them with the null keyword. When you qualify a pointer declaration with both array and null, it does not matter which order you place the qualifiers in; however we suggest using array null rather than the other way round.
When declaring a function parameter that accepts an array of elements of some type T, both C and C++ allow the type to be declared as T[ ] as an alternative to T*, with the same meaning. eCv also allows T[ ] as the type of a parameter to be qualified with null; so declaring a parameter with type T[ ] null has the same meaning as declaring it with type T* array null.
Sometimes you may have an expression that has a nullable pointer type, but you know that its value is not null and you wish to use it in a context that requires a non-nullable pointer. You can do this using the not_null construct.
The expression not_null(pointer-expression)
yields the value of pointer-expression (which must have nullable pointer or nullable array pointer type) as a non-nullable
pointer or non-nullable array pointer, asserting that it is not null.
This is equivalent to a cast from the nullable type to the non-nullable type, but avoids your C compiler or other static checker perhaps
issuing a warning about a redundant cast. It also makes it clear that you are just asserting non-nullness, rather than trying to do a more
general type conversion. eCv will generate a verification condition that pointer-expression is not null.
If you use an expression whose type is a nullable pointer type in a context where a non-null pointer is required, eCv will assume an implicit not_null(...) operation around the expression, and warn you that it has done so.
Parameters of pointer type are often used to pass values results between functions and their callers. When you declare a parameter of a non-const pointer type, eCv normally assumes that when you call the function, it both reads and writes the value that is pointed to. Therefore, if you take the address of a variable and then pass that address to a function, you must initialize that variable first. The function is permitted but not obliged to update the variable by writing through the pointer.
You can change this behaviour by flagging a parameter with the keyword out at the start of its declaration. This indicates to eCv that the pointer parameter is used only to pass a value back from the function. When you take the address of a variable and then pass that address as the actual value of an out parameter, you do not need to initialize the variable first. However, a function is obliged to write through all its pointer parameters that have been flagged as out parameters, except when the parameter is a nullable pointer and the actual parameter is null.
Here is an example:
void foo(int *p, out int *q, out int *r) {
p += 1; /* ok */
q += 1; /* error, out-parameter q used before it has been initialized */
return; /* error, function must initialize out-parameter r before returning */
}
...
int a, b, c, d;
foo(&a, &b, &c); /* error, 'a' has not been initialised */
foo(&b, &c, &d); /* ok, 'b' was initialized by the previous call to foo */
Only parameters of non-const pointer type (including pointer types flagged array and/or null) may be flagged out.
If you use assertions in your program and #include "assert.h" in your source file, we suggest that you make this inclusion conditional like this:
/* #include "ecv.h " somewhere before the following */
#ifndef __ECV__
#undef assert /* remove eCv's definition */
#include "assert.h"
#endif
eCv will then treat your assertions as eCv assertion statements (see assert) and try to prove they are true.
If you do not make the inclusion conditional, then the definition of assert in file assert.h may override the definition of assert in file ecv.h. If the DEBUG macro is defined when you run eCv, then your assertions will typically be expanded to code that performs I/O if the assertion fails. eCv will try to verify this code and will report errors if it modifies variables that were not declared in the writes-clause of the current function.
eCv supports the following extensions to the C and C++ languages as defined in the ISO standard documents:
Many C and C++ compilers support additional extensions. Where these extensions are implemented using additional keywords (possibly followed by a bracketed argument list), it is usually possible to define these keywords as null macros when processing with eCv, so that eCv does not see those extensions and can process the source file. File eCv.h already contains a number of these macro definitions.
Sometimes you may find that your C compiler accepts your source code, but eCv does not. Here are some of the most common eCv error messages that you may see under these conditions, and what they mean.
Error! Incorrect syntax at ... Assuming
that a regular C compiler accepts your source code, then this means one of the following:
Error! Incorrect syntax at token '_ecv_pre'.
This can occur if you have extra brackets around the function declarator, e.g.
int (foo(int arg)) pre arg > 0 { ... }
The fix is either to remove the extra brackets:
int foo(int arg) pre arg > 0 { ... }
or to include the precondition (and any other specifications) inside the brackets:
int (foo(int arg) pre arg > 0 ) { ... }
Error! Cannot find declaration of class 'size_t'.
This will occur if your program uses the C sizeof keyword, but you haven't included
any standard header file that defines size_t.
eCv needs this definition so that it knows exactly what type a sizeof
expression yields. The fix is to #include stddef.h (or some other header that
correctly defines size_t) in your source file.
Error! Cannot find declaration of class 'ptrdiff_t'.
This will occur if your program subtracts one pointer from another,
but you haven't included any standard header file that defines ptrdiff_t.
eCv needs this definition so that it knows exactly what type a pointer difference expression
yields. The fix is to #include stddef.h (or some other header that
correctly defines ptrdiff_t)
in your source file.
Error! No binary operator '==' defined between types 'T*' and 'int' (for some T, where the integer operand is
literal zero, and where == can also be !=). This normally
indicates that the variable or parameter of type T*
should have been declared nullable, i.e. T* null instead of just T*.
Error! No binary operator '+' defined between types 'double' and 'int' (for '+' or some other arithmetic operator). eCv
does not support mixed-mode arithmetic. Cast the integral operand to double
or some other suitable floating-point type.
Error! No globals or current class members can match 'result'. This occurs when you use an expression like 0..result
in a specification and you are using your compiler's own preprocessor.
The reason is that the preprocessor treats 0..result as a single pp-number token, so it doesn't recognise result as a macro to be expanded.
To fix this, put a space between 0 and ..
or between .. and result,
or use (0) instead of 0,
or use (result) instead of result.
If your code uses either an eCv
specification macro such as pre or
one of your own macros, and eCv detects errors either in the code resulting
from the macro expansion or in code that follows the macro and its
arguments on the same line, then the line/column coordinates that
eCv provides in the error message may to be incorrect. This is because eCv
sees the code after macro expansion.
If you put specification macros and their actual parameters all on the same line, and you do not use any other macros on that line, then the line number should be correct. If you are using the eCv preprocessor or your compiler's preprocessor preserves white space, and you use the standard eCv specification macro names, then the column numbers should also be correct.
If you use keywords starting with _ecv_ directly, then the column number of any message that refers to a construct after that keyword but on the same line will be incorrect. This is because when eCv calculates the column number in the original source file, it assumes that any keyword starting with _ecv_ was generated by expanding the corresponding keyword without the _ecv_ prefix.
If you put macro parameters on more than one line, then your preprocessor may expand the macro such that everything is on one line. In that case, any error messages relating to code or specifications in the macro parameters will have a line number that relates to the source line on which the macro name appeared; and the column number may be somewhat higher than the number of columns in that line. For this reason, we suggest that, when declaring specifications, you keep each specification and its arguments on the same line, wherever possible. For example, don't use:
pre(a >= 0;
a < 10)
Instead, use either:
pre(a >= 0; a < 10)
or:
pre(a >= 0)
pre(a < 10)
You can suppress a warning message (but not an error message) like this:
#pragma ECV ignore_warning "warning-text"
This will cause a single instance of a warning message that includes the specified text to be ignored. Instead, an information message will be generated that the warning has been ignored. You can list multiple comma-separate warning messages in a single pragma. Here is an example:
void f(int a, unsigned int b) {
#pragma ECV ignore_warning "Signed/unsigned mismatch", "Implicit conversion of expression 'a + b'"
int c = a + b;
Optionally, you may give an integer line offset before the first message, to specify the number of lines to be skipped before the warning message is expected.
Here is another way of expressing the previous example:
#pragma ECV ignore_warning 2 "Signed/unsigned mismatch"
#pragma ECV ignore_warning 1 "Implicit conversion of expression 'a + b'"
void f(int a, unsigned int b) {
int c = a + b;
eCv will warn you if you use the ignore-warning pragma but no matching warning is generated.
eCv Manual, Version 7.0, February 2017.
© 2017 Escher Technologies Limited. All rights reserved.