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

[Frama-c-discuss] (no subject)



Thank you for the answer, Clauude. Yes, "new_value" is my attempt to mimic
malloc (I abstracted the details out). Reason why I started doing it in
the first place was that WP displayed the warning: "warning: Allocable,
Freeable, Valid_read, Fresh and Initialized not yet implemented".
As it is under "experimental" section in ACSL documentation, I concluded
it is just not yet implemented.
(I have problems with Jessie, it crashes and I still don't get why, so I
couldn't try with it.).
Which prover do you use? (that supports those "experimental" features)


>
> As said others before, your contract on main() is not valid.
>
> As the name "new_value" suggests, do you expect that this function
> returns a freshly allocated pointer? In that case, your contract should
> reflect this. Here is a possible specification. Notice also that your
> initial ensures "\result != \null" is not enough to guarantee that the
> resulting pointer is \valid
>
>
> /*@ assigns \nothing;
>   @ allocates \result;
>   @ ensures \valid(\result) && \fresh(\result,sizeof(int*));
>   @*/
> extern int *new_value();
>
> /*@ requires \valid(p);
>   @ assigns *p;
>   @*/
> void f(int* p){
>   *p = 8;
> }
>
> /*@ assigns \nothing;
>   @*/
> int main(void){
>  int *p = new_value();
>  f(p);
> }
>
> Side note: the allocates clause might not be well supported by plugins
> WP and Jessie. With Jessie, such a code triggers an error, unless you
> add the pragma
>
> #pragma SeparationPolicy(none)
>
> (this is a known bug of the separation analysis in presence of dynamic
> allocation)
>
> - Claude
>
>
>
> On 10/31/2014 04:09 PM, gavran at mpi-sws.org wrote:
>> 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
>