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 and SystemC

  • Subject: [Frama-c-discuss] Frama-c and SystemC
  • From: Xingyu.Zhao.1 at city.ac.uk (Zhao, Xingyu)
  • Date: Thu, 22 May 2014 17:42:07 +0000
Dear All,

Recently, I am analysing a C software which has been encapsulated by SystemC for simulation purpose. So actually there are some c++ codes and  library functions of SystemC in the C codes which I want to analysis in framaC. For example:

for (;;) {
        out = false;
        wait(in.posedge_event());
        out = true;
        wait(length);
}

The wait() function is from the SystemC library. I do not think frama-c or WP can proof something related to that, right? And is there any tool in frama-C could analysis something related to the time. Or does ACSL support to describe some time issues so I could proof them with WP.

Any help will be appreciated.

Regards,
Xingyu.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140522/70975947/attachment.html>