--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on September 2009 ---
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