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

[Frama-c-discuss] Examples for external spec file support of ACSL



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