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] ACSL Parsing



Hello,

On 12/07/2011 04:20 PM, Boris Hollas wrote:
> On Wed, 2011-12-07 at 15:36 +0100, Julien Signoles wrote:
>> To answer to one of the primary questions, the C+ACSL Frama-C's AST is
>> fully documented in file cil/src/cil_types.mli which is available in the
>> last open-source release (http://frama-c.com/download.html).
> There is a Cil documentation athttp://www.eecs.berkeley.edu/~necula/cil/,  including a documentation of the visitor.

I guess that the right link is http://kerneis.github.com/cil/doc/html/cil

Is this document useful to understand Frama-C's AST?

It could be, but Cil only covers the C part of the AST, not the ACSL 
one. Moreover, there are now several (usually minor but incompatible) 
differences between the C part of the Cil AST and the Frama-C one. 
Additionally, in Frama-C, the Cil visitor is overloaded by the Frama-C 
one. This last visitor handles ACSL annoations and preserves Frama-C 
internal invariants, but it is a little bit more complex to use (see 
Section 5.14 of [1]). Thus I have to say that it is more reliable to 
read Frama-C documentations [1,2]  than to read Cil documentation in 
order to understand the Frama-C's AST.

[1] Frama-C Plug-in Development Guide. 
http://frama-c.com/download/plugin-development-guide-Nitrogen-20111001.pdf
[2] Frama-C API Documentation. 
http://frama-c.com/download/frama-c-Nitrogen-20111001_api.tar.gz

Best regards,
Julien