--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on November 2011 ---
More specifically, let's assume I have the function void foo(bar *this) { this->x = 0; } and I want to add the postcondition ensures this->x == 0; Can this be accomplished as a Frama-C-plugin? If so, how can I access parse tree and symbol table of the parsed code via Frama-C? -- Best regards, Boris -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111118/697f9522/attachment.htm>