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