Taking the address of a formal in a function contract

[vprevosto]

(backported from Frama-C's bts)

In 0002390 the issue was raised whether functions contracts such as

/*@ requires
    \valid(&a);
    ensures \false; */
void f(int a) {
  return ;
}

are meaningful. More specifically, the ACSL manual should clarify whether using the address of a formal argument in a precondition, and more generally a function contract, is illegal.

[yakobowski]

Loïc's said under https://bts.frama-c.com/view.php?id=2390 that

[in the WP] formals are not (yet) allocated in the pre-state, although they are allocated just before the first statement of the body...

This seems strange to me, as the pre-state can (of course) refer to the value of formals. And, if we accept that they are in scope in the pre-state, I don't see why we would reject terms that take their address. This is probably not very useful, but not worth rejecting either.

In the post-state, Frama-C's kernel has already taken a stance, since we add \old around the use of formals.

[vprevosto]

@yakobowski I tend to agree with the fact that this is a bit strange, but at the same time, the fact that formals retain their original value in the ensures clause is an indication that they are a bit special. It might make sense to treat them as some variant of C++ reference (i.e. whose address cannot be taken).

[jensgerlach]

I also think it is strange to say the formals are not (yet) allocated in the pre-state because we talk about their values in the preconditions.

I tend to reject taking the address of a formal argument in the contract. (It might of course be useful to take the address in the function body.)

Is there a meaningful usage of such an address for the caller ? I somehow doubt it and consider it as dangerous as returning the address of a local variable.

On the other hand, it might be "necessary" in a contract to take the address because there is a predicate that has a pointer argument

//@ predicate Positive(int* a) = *a > 0;

/*@
   requires Positive(&n);
*/
int foo(int n);

Should one disallow/discourage such predicates?

[vprevosto]

The caller does not have access to the addresses of the formals indeed, but your example of a predicate taking a pointer as argument is interesting (even though I'd expect to see pretty few examples of that in real applications).

[yakobowski]

Well, we tend to create predicates taking pointers as arguments since we cannot reason on sets of locations without this mechanism.

Regarding e.g. addresses of formals in the post-state, I was going to suggest banishing them when not under a \at(_, Pre), but this is hard to do with predicates taking labels as arguments...

[jensgerlach]

Virgile mentioned references. Maybe one could used references in ACSL predicates... (My apologies, if this is a sacrilege!-)

[pbaudin]

Of course, it could be useful to take the address of formals, but as far I remember, specifications taking such an address can be always rewritten without taking that address. Here there is two example where in C the address of formals has to be taken, but this is not necessary in the ACSL specifications:

//@ predicate P1(int t[3]) = t[0] >= t[1] + t[2] ;
//@ requires  P1( (int [3]) p ); // this cast is allowed in ACSL
void g1 (int p[/*3*/]) ; // note: p is a pointer

struct st_T1 { int tab[3]; };
//@ requires P1(st.tab);
void f1 (struct st_T1 st) {
   g1( &st.tab[0] );
}

//@ predicate P2(struct st_T1 st) = P1( st.tab ) ;
//@ requires  P2( st );
void g2 (struct st_T1 st) ;

struct st_T2 { int a1, a2, a3; };
//@ requires P2( (struct st_T1)(st) ) ; // this cast is allowed in ACSL
void f2 (struct st_T2 st) {
   g2( *(struct st_T1 *)(&st) );
}