Eva: Differs from C specification on pointer arithmetic
-
the issue has not yet been reported on Gitlab; -
the issue has not yet been reported on our BTS; -
you installed Frama-C as prescribed in the instructions.
I believe I have followed the third bullet, but it isn't clear if that means just making sure to properly install with Opam, or if I am expected to manually compile the newest version, and test it (which I haven't done).
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 20.0 (Calcium)
- Plug-in used: Eva
- OS name: Linux Mint
- OS version: Linux 4.15.0-99-generic #100 (closed)~16.04.1-Ubuntu SMP
Please add specific information deemed relevant with regard to this issue.
Steps to reproduce the issue
Run the following test function through the Eva plugin:
void test(void) {
int a[] = (const int[]) { 5 };
int* b = &a;
/*@ assert \offset(b) == 0; */
int* c = b + 1;
/*@ assert \offset(c) == 1; */
}
Expected behaviour
For both of the assertions to succeed as the C89, and C99 specification taking a pointer one past the end of a C array is allowed (dereferencing that pointer is not). Therefore both checks should succeed from what I can tell.
Actual behaviour
It claims that the second assertion fails as it is invalid:
[eva:alarm] src/test_array.c:6: Warning:
assertion got status invalid (stopping propagation).
Fix ideas
I assume it is a bug with Eva, and not with the core Frama-C system, but I could be mistaken. Please note that the idea of one past an array also applies to non-array objects.
For the purposes of these operators. a pointer to a nonarray object behaves the same as a pointer to the first element of an array of length one with the type of the object as its element type.
Meaning the following should also succeed:
void test(void) {
int a = 5;
int* b = &a;
/*@ assert \offset(b) == 0; */
int* c = b + 1;
/*@ assert \offset(c) == 1; */
}