Taking the address of a formal in a function contract about acsl HOT 7 OPEN

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.

from acsl.

@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).

from acsl.

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?

from acsl.

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).

from acsl.

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...

from acsl.

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

from acsl.

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) );
}

from acsl.