--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on April 2011 ---
Hi, Le 28/04/2011 09:30, Steven Gong a ?crit : > I found in the Carbon code, there seems to be external spec file support > of ACSL, noted by > (* ACSL extension for external spec file *) > But I cannot find any examples in either the ACSL manual or test code. > Does anyone know the status of this support? Is there any example on how > to use the feature? Thanks. External ACSL specification support is not available in the Open Source distribution of Frama-C. A specific plugin implementing such a support exists, is commercially available and can be obtained from the CEA LIST/LSL. We can discuss your specific needs off-list if you are interested. It seems to me that such a plugin becomes useful as soon as you intend to start the industrial deployment of parts of Frama-C: having a dedicated support contract about Frama-C is probably not avoidable in this settings as specific plugins and/or plugin's adaptations may be necessary. Depending on your exact intentions R&D, support, or any other kind of service, can be provided either directly by CEA LIST/LSL or by a few other dedicated service companies. Could you share some informations about your use case and needs so that we can understand which of the available options may be appropriate? Thanks a lot for your interest in Frama-C, do not hesitate to continue this thread off list or on list depending on your constraints, -- Benjamin Monate Head of Software Safety Lab. CEA-LIST/DRT/DILS/LSL