--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on October 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] (no subject)



Hi,

I have a problem with assigns clause. Assume the following code:

/*@ ensures \result != \null;
  @ assigns \nothing;
  @*/
extern int *new_value();

//@ assigns *p;
void f(int* p){
  *p = 8;
}
//@ assigns \nothing;
int main(void){
 int *p = new_value();
 f(p);
}

The prover is unable to prove that main assigns \nothing, which makes
sense, as main assigns to *p through function f. However, how should I
state that in \assigns clause, since p is local variable and can not be
accessed within annotation?

Ivan
p.s. I repeat the question posted on SO -
http://stackoverflow.com/questions/26591694/assigns-clause-for-local-variables-in-frama-c