--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on September 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie - type invariants



Hello Kerstin,

Le lun. 21 sept. 2009 10:05:32 CEST,
"Kerstin Hartig" <kerstin.hartig at first.fraunhofer.de> a ?crit :

> Anyway, there are syntax errors when using the strength modifiers weak or
> strong. (using both - global or type invariants)
> Is this a case for a bug report or is it supposed to not work yet?

It is not supported by the implementation yet. Note that the ACSL at
http://frama-c.cea.fr/download/acsl_1.4.pdf presents the ACSL language
itself, without any reference to the implementation of it in Frama-C.
A version containing implementation notes can be found in the
distribution you have installed and at the following address. 
http://frama-c.cea.fr/download/acsl-implementation-Beryllium.pdf
In this latter document, every construction that appears in red is not
supported in Beryllium. Note in addition that  "supported" in this
context only means type-checks. Support by a particular plug-in (such
as jessie or the value analysis) is yet another matter, and the status
should be found in the relevant plug-in manual (of course, a feature
which not supported by the core is not supported by any plug-in).

I hope this clarifies a bit the status of ACSL support in Frama-C. If
there are some ACSL features missing in the implementation that you
find very important, feel free to add a feature wish to the bts. This
will help us assigning priorities for supporting ACSL constructions.

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile