--- layout: fc_discuss_archives title: Message 30 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



Hi all,

Thanks Pascal for noticing the mistake in the pointer to the PLPV article.

Coming back to the first request, Barbara wants a "specification of the 
semantics" of the Jessie language,
and the 2 pages PLPV paper will certainly not answer to that.

Given that fact that even the syntax of it evolved a lot in time, I'm 
afraid I cannot propose any up-to-date document.
If you have a specific point in mind, please ask.

- Claude





On 01/18/2011 02:03 PM, Pascal Cuoq wrote:
>> On Tue, 2011-01-18 at 12:49 +0000, Barbara Vieira wrote:
>>      
>>> I'm working the Jessie plug-in from the Frama-C framework and I would like to know if somebody knows if there is any document specifying the semantics of the Jessie language.
>>>        
> On Tue, Jan 18, 2011 at 1:56 PM, Boris Hollas
> <hollas at informatik.htw-dresden.de>  wrote:
>    
>> There's no Jessie specific language. The language used by Jessie is
>> ACSL, which is documented on frama-c.com.
>>      
> Yes, there is. Jessie is an intermediate language before being a
> Frama-C plug-in.
>
> The theoretical aspects are described here:
> http://portal.acm.org/citation.cfm?doid=1292597.1292598
> (Claude, if you see this, fix your
> http://www.lri.fr/~marche/biblio.html page, it sends to the wrong ACM
> article).
>
> Pascal
>
> _______________________________________________
> 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                    |