--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on August 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about hybrid logic functions



sorry, I should have used struct pointers originally :

struct stack {
  //@ ghost abstract_stack my_abstraction;
} st;

/*@ axiomatic A {
  @    logic integer count_of{L} (Stack *s) reads s->my_abstraction;
  @*/

/*@ requires 0 < count_of{Here}(st);
  @ assigns st.my_abstraction;
  @ ensures  count_of{Here}(&st) == count_of{Old}(&st) - 1;
  @*/
void pop(void)


Anyway, passing structures by value to a predicate deserves a better explaination in ACSL.

At least, I'm sure that it does not work has intended with the Jessie plugin.


- Claude



BAUDIN Patrick wrote:
>
>>>  /*@ requires 0 < count_of{Here}(st);
>>>   @ assigns st.my_abstraction;
>>>   @ ensures  count_of{Here}(st) == count_of{Old}(\old(st)) - 1;
>>>   @*/ 
>>>
>>> in fact, the labels {Here} and {Old} given to count_of are insignificant
>>>   
>>>     
>> Wrong again. It is the \old(st) which is useless: st is not modified by 
>> the function so \old(st)==st.
>> In the other hand, count_of{Old}(st) is a priori different from 
>> count_of{Here}(st) since count_of
>>  reads st.my_abstraction and this is said to be assigned.
>>   
> I can't see is how you can 
>   
>  @ assigns st.my_abstraction
> and
>   
>  @ ensures \old(st)==st
>
> in a same specification ?
>
> Patrick.
>   
> ------------------------------------------------------------------------
>
> _______________________________________________
> 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


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |