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

[Frama-c-discuss] (no subject)



Thanks for the answer. However, upon verifying it, I get
wp failure: Address of logic value (L_R).
Which plugin did you use to prove it?

Ivan

off question: what is prefered way communication? Should I continue
discussion on the mailing list or on Stack Overflow?

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