Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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