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] frama-c boron inconsistency with beryllium

  • Subject: [Frama-c-discuss] frama-c boron inconsistency with beryllium
  • From: kalyan.krishnamani at gmail.com (Kalyan)
  • Date: Mon, 10 May 2010 10:28:18 +0200
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>