--- layout: fc_discuss_archives title: Message 31 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 02:31 PM, Boris Hollas wrote:
> On Tue, 2011-01-18 at 14:03 +0100, Pascal Cuoq wrote:
>    
>> Yes, there is. Jessie is an intermediate language before being a
>> Frama-C plug-in.
>>      
> I see, you mean the language that the annotated C code is converted to
> by Jessie. Yannick Moy's PhD contains a section on the Jessie language
> http://www.lri.fr/~marche/moy09phd.pdf.
>    

Indeed, but be careful that this description and the current implementation
may differ. So if it helps, that's perfect, otherwise please ask.

- Claude


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