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] Pointer to Jessie input language semantics

On 01/18/2011 03:52 PM, Barbara Vieira wrote:
>
>> Indeed, but be careful that this description and the current implementation
>> may differ. So if it helps, that's perfect, otherwise please ask.
>>      
> Claude, I think that it really helps a lot! I'll take care with the different aspects.
> Anyway, I took a quick look at the Yannick thesis and as far as I understood it does not specify the semantics (neither the syntax) of the axiomatic statements, logic functions and logic variables.
>    

Yes, but this is supposed to be identical to the ACSL ones, so the ACSL 
spec lang is the reference.

> I will try to do it by myself. I'll contact you again if any doubt come up.
>    

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