Eva for function prototype returning pointer to array

user_17677483 0
Viewed 45

I have a question regarding using Eva for functions that return pointers, I am using Frama-C version 23.1 (Vanadium). The issue arises when only the prototype, and not the body, of the function is available, and the assumption is that the function should return a pointer to the beginning of an array. Below is a minimal example:

int arr[8];
int x,y;

int *foo();

// int *foo() {
//   return arr;
// }

void main() {
  int *a = foo();

  x = a[2];

  y = 3;
}

The analysis stops upon reaching the line x = a[2] and generates the following alarm from the associated memory assertion:

alarm: assert Eva: mem_access: \valid_read(a + 2);
Status: **NOT** VALID according to Eva (under hypotheses)

This instruction always fail.

If I provide the body of the function (which is commented out in the example), the analysis works. However, I wonder if there is some way to fully analyze this program using Eva, without providing the body, for example by annotating the foo prototype in ACSL. I tried using the allocation clause of ACSL function contracts, but it seems not supported by Eva. Perhaps there is some other annotation that I have not found or some other way of configuring Eva to allow analysis of this program?

Any help would be greatly appreciated.

frama-c
1 Answers

Indeed, if you don't want (or can't) provide the body of f, Eva will require some additional input, generally under the form of an ACSL contract or by writing a stub directly in C, allowing for a simpler representation than the full-fledged definition (Section 5.4.3 of the Eva manual briefly describes these two points).

If you take the ACSL contract route, you first have to write an appropriate assigns clause(s), including the \from part, which is needed for Eva to have an accurate view of the dependencies between memory location.

You can also provide requires clause, to check that the function is called in a suitable context, and ensures clause to be more precise about the value taken by the locations mentioned in the assigns clause. In both cases, the ACSL clauses should be interpretable by Eva, otherwise they won't be really useful. Chapter 8 of the Eva manual deals with the handling of ACSL annotations by Eva.

In your particular context, a possible contract for f would be the following:

int* b = &arr[0]; // Eva does not seem to appreciate &arr[0] in the \from
/*@ assigns \result \from b;
    ensures \result == &arr[0];
*/

Note that allocates clauses and \fresh/\freed ACSL predicates are not among the subset of ACSL that is understood by Eva, so that if you want to deal with functions that perform dynamic allocation, you'll need to take the C stub route.

user_16336650
Related