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] issues with the ACSL Post label

  • Subject: [Frama-c-discuss] issues with the ACSL Post label
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Sun, 1 Dec 2013 20:44:17 -0500
  • In-reply-to: <CAEt_dErdeRPm0FQon35=E=vx8Od6w-cXXeASxv8B+4P52tM0ag@mail.gmail.com>
  • References: <BAY169-W791B99FF16C894E692A16C97E90@phx.gbl>, <CAA1cxuhbHXpRvQbopVBNsqNGzVKGAUS1j=xSK-kBr51ggF5nLQ@mail.gmail.com>, <CAEt_dEoZSi6Dgak2Upo4NyaziBRnJmB=LXHTfxaSd0iRni4gKQ@mail.gmail.com>, <CAEt_dErdeRPm0FQon35=E=vx8Od6w-cXXeASxv8B+4P52tM0ag@mail.gmail.com>
Hi,
   Thanks for the helpful comments! 
   I will try to avoid the usage of "Post" label in the ensure clause. Just for the knowledge of ACSL, is it safe to say that in the ensures clause the "Post" label is implicitly assumed to refer post state? And "Here" label in the ensures clause actually refer to the post state as well?
for instance, suppose I would specify a function of which post state is a==0 :
    ensures a==0;      
    <==>
    ensures \at(a, Here)==0;     /* "Here" refers to the state after function execution?*/
    <==>
    ensures \at(a, Post)==0;

   thanks..

cheers,
xiao-lei

To: frama-c-discuss at lists.gforge.inria.fr
Subject: Re: [Frama-c-discuss] issues with the ACSL Post label

Perhaps I should've been more explicit:

   Here is equivalent to Pre
This is not true. the Here label refers to the state in which the annotation is evaluated. eg: when used with requires, it refers to the pre-state, when used in ensure it refers to the post-state, when used in loop invariants it refers to the current iteration.

Omitting the \at clause or using \at( _ , Here) is equivalent, as such: *a == \at(*a, Here) will always hold

   By removing the 'Post' label from above annotation, the VCs can be generated and proved.

Like I said before, omitting the \at clause is equivalent to \at(*a, Here)

   Pre  is equivalent to Old ?

Yes, \old(*a) == \at(*a, Pre)

-- 
Cumprimentos,Cristiano Sousa


_______________________________________________
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 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131201/6cd643dd/attachment.html>