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] Examples for external spec file support of ACSL

  • Subject: [Frama-c-discuss] Examples for external spec file support of ACSL
  • From: benjamin.monate at cea.fr (Benjamin Monate)
  • Date: Thu, 28 Apr 2011 12:14:07 +0200
  • In-reply-to: <BANLkTi=TseMJS87ss9r1joQ4Hi+YCKxdbg@mail.gmail.com>
  • References: <BANLkTi=TseMJS87ss9r1joQ4Hi+YCKxdbg@mail.gmail.com>
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