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] How to see non-ACSL comments in Frama-C AST?

On Fri, Mar 18, 2011 at 3:14 PM, Etienne Lozes <lozes at lsv.ens-cachan.fr> wrote:
> I am wondering if this is possible to see the original comments of a C code
> in the
> AST?
>
> I tried to match the Gtext construct of the type Cil_types.global, but
> either I did not do it
> correctly (I am new to Frama-C), or the purpose of GText is orthogonal to
> comments.

Hi Etienne,

Cil_types.GText are intended for plugin developers to add their own
(non-interpreted) information to the ast. You are correct, this
mechanism is not used to store comments. This would not work anyway:
you can only have a GText at toplevel, and not at the level of
statements.

If you want to add structured information, you can try to use ACSL
specifications, with your own custom predicates. This is probably the
cleanest solution, and is well-supported by the kernel.

Alternatively, comments are kept if you specify the option
-keep-comments of Frama-C. They are however still not exposed directly
through the Ast. You can access them through the function
Zrapp.get_comments (I have enclosed an example in the attached file).
Notice that using this function is not easy: calling it will remove
the comment forever. In particular, you will break Frama-C -print
option. You can, and should, follow what is done by Frama-C itself:
get_comments is only called in the method pLineDirective, which is
itself called only non-composite statements, or on globals. To
summarize, this is possible, but not for the faint of heart.

Hope this helps,

-- 
Boris
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.ml
Type: text/x-ocaml
Size: 695 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110321/ce4b4ef2/attachment.bin>