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

[Frama-c-discuss] (no subject)



The only way to handle your situation, is to make the result of new_value accessible from the logic space.
For instance :

//@ logic int * R ;
//@ ensures \result == R && \valid(R) ; assigns \nothing ;
extern int *new_value();

//@ assigns *p;
void f(int * p) { ? }

//@ assigns *R ;
int main(void) { ? }

A more general solution would be to have a set if pointer for R, instead of a unique one.
	L.

Le 31 oct. 2014 ? 16:09, gavran at mpi-sws.org a ?crit :

> 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
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss