--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on January 2011 ---
[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                    |