--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on December 2011 ---
[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