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
- Subject: [Frama-c-discuss] ACSL Parsing
- From: Julien.Signoles at cea.fr (Julien Signoles)
- Date: Wed, 07 Dec 2011 18:23:49 +0100
- In-reply-to: <1323271226.2391.45.camel@iti27.informatik.htw-dresden.de>
- References: <000901ccb0fb$6411f4c0$2c35de40$@informatik.uni-freiburg.de> <000701ccb10f$38f61960$aae24c20$@informatik.uni-freiburg.de> <4EDF7538.8080701@inria.fr> <4EDF79D1.9080301@cea.fr> <1323271226.2391.45.camel@iti27.informatik.htw-dresden.de>
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
- References:
- [Frama-c-discuss] ACSL Parsing
- From: lindenmm at informatik.uni-freiburg.de (Markus Lindenmann)
- [Frama-c-discuss] ACSL Parsing
- From: Claude.Marche at inria.fr (Claude Marche)
- [Frama-c-discuss] ACSL Parsing
- From: Julien.Signoles at cea.fr (Julien Signoles)
- [Frama-c-discuss] ACSL Parsing
- From: hollas at informatik.htw-dresden.de (Boris Hollas)
- [Frama-c-discuss] ACSL Parsing
- Prev by Date: [Frama-c-discuss] ACSL Parsing
- Next by Date: [Frama-c-discuss] ACSL Parsing
- Previous by thread: [Frama-c-discuss] ACSL Parsing
- Next by thread: [Frama-c-discuss] ACSL Parsing
- Index(es):