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

Hi,

At this time, support for C++ is not yet available for Frama-C, hence, neither for SystemC.
We are working on a C++ front-end for Frama-C, but it is not yet mature enough for an official release.

However, since your software is written C (but encapsulated in C++), you can mimic the way SystemC invokes your software by crafting one or several dummy ?main? functions, and prove your program under these ?scenarios?. This is the usual way we proceed, even for pure C-programs, to decompose a complex verification task into several, tractable ones.

Time is not supported in ACSL. The (distributed) plug-in Aorai can be used to specify sequences of function calls during execution (through automaton or LTL), which is a kind of timed specification. Such automaton are then translated into regular ACSL annotations, which must be proved in turn.

The GATeL platform is dedicated to the proof of Lustre program properties, is much more adapted to verify timed-properties.
It is another mature technology developed in our lab, but there is no link between Frama-C and GATeL already available (work in progress). As an effective methodology, you should consider proving with GATeL a timed-property on a Lustre/Scade model of your code, then, use Frama-C to unitary prove that each component of your code behaves (at any time) the same way than the corresponding Lustre/Scade part of the model.

	L.

Le 22 mai 2014 ? 19:42, Zhao, Xingyu <Xingyu.Zhao.1 at city.ac.uk> a ?crit :

> 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.
>  
>  
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss

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