--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] frama-c boron inconsistency with beryllium



Hi,
       I tried the syntactic_check plugin from frama-c plugin manual,
and it does not seem to work as expected:

1. the order of arguments to Visitor.generic_frama_c_visitor () is different
(also in Beryllium)
2. the frama-c-gui does not show the assertion generated (and added to the
statement); it was
    showing up with Beryllium version.

It would be great if you could let me know of any alternative way for me to
check if the assertion
has been added or not. Also, how to run any user-written plugin along with
already available
plugins like jessie. (As I would like to have a plugin that generates
annotations, and then call
jessie to verify if the annotations/assertions hold)

Kalyan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100510/b0657329/attachment.htm>