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

[Frama-c-discuss] Frama-c and SystemC



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>