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