Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] (no subject)

  • Subject: [Frama-c-discuss] (no subject)
  • From: gavran at mpi-sws.org (gavran at mpi-sws.org)
  • Date: Sat, 1 Nov 2014 19:10:10 +0100
  • In-reply-to: <5453DE5E.4070401@inria.fr>
  • References: <ddc718fd7d0e66a4f3e5121676cf59e2.squirrel@mail.mpi-sws.org> <5453DE5E.4070401@inria.fr>
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
>