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; */
}