Frama-C-discuss mailing list archives

Xingyu.Zhao.1 at city.ac.uk (Zhao, Xingyu) · Sat, 24 May 2014 15:54:09 +0000

Dear All,

Thanks for your help in my last email " Frama-c and SystemC ". Mr. Correnson replies that

 " 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." 

it indeed opened my thoughts. But one more question related to this.

Actually I am not interested in the time-sequence of function calls. What I want to proof is something like, for simplification, both input and output variables are 0 at beginning, when I set input variable to 1, then after 10 seconds, the output will change to 1 accordingly. How to proof this kind of time-related informal requirements with frama-C?

Regards,
Xingyu.

-----Original Message-----
From: frama-c-discuss-request at lists.gforge.inria.fr [mailto:frama-c-discuss-request at lists.gforge.inria.fr] 
Sent: 2014?5?23? 9:56
To: frama-c-discuss at lists.gforge.inria.fr
Subject: Frama-c-discuss Digest, Vol 72, Issue 10

Send Frama-c-discuss mailing list submissions to
	frama-c-discuss at lists.gforge.inria.fr

To subscribe or unsubscribe via the World Wide Web, visit
	http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
or, via email, send a message with subject or body 'help' to
	frama-c-discuss-request at lists.gforge.inria.fr

You can reach the person managing the list at
	frama-c-discuss-owner at lists.gforge.inria.fr

When replying, please edit your Subject line so it is more specific than "Re: Contents of Frama-c-discuss digest..."

Today's Topics:

   1. Frama-c and SystemC (Zhao, Xingyu)
   2. extended_Euclide (MAXIM GAINA)
   3. Re: Frama-c and SystemC (Lo?c Correnson)

----------------------------------------------------------------------

Message: 1
Date: Thu, 22 May 2014 17:42:07 +0000
From: "Zhao, Xingyu" <Xingyu.Zhao.1 at city.ac.uk>
To: "frama-c-discuss at lists.gforge.inria.fr"
	<frama-c-discuss at lists.gforge.inria.fr>
Subject: [Frama-c-discuss] Frama-c and SystemC
Message-ID:
	<9d40897fa4894216ba17fc20b00bab07 at DB4PR03MB410.eurprd03.prod.outlook.com>

Content-Type: text/plain; charset="us-ascii"

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-0001.html>

------------------------------

Message: 2
Date: Fri, 23 May 2014 09:50:39 +0200
From: MAXIM GAINA <maxim.gaina at studenti.unipr.it>
To: frama-c-discuss at lists.gforge.inria.fr
Subject: [Frama-c-discuss] extended_Euclide
Message-ID:
	<CAFq8hrzf5R5hjv7u7_YXYjr89GLrJ1YZ4kgkkudtbWux9SEfRQ at mail.gmail.com>
Content-Type: text/plain; charset="utf-8"

Good morning.

While training on Frama-C in a Semanthics class, I tried the example shown on page 41 of ACSL handbook ( http://frama-c.com/download/acsl-implementation-Neon-20140301.pdf), which exemplifies a possible implementation of Extended Euclide Algorithm.
However, I was not able to proof any relevant property: am I missing something?

The code is attached. I am using Frama-C Neon on a 64-bit Fedora 20. I used Alt-Ergo (Native) as theorem proover, having enabled both RTE and Invariants. The Bezout property could not be proved in the contract (orange
ball) but is partially proved before the while loop, inside the function (green/red ball).

Waiting for an answer, I offer my best regards
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140523/c79446a6/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: extended_Euclid.c
Type: text/x-csrc
Size: 566 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140523/c79446a6/attachment-0001.c>

------------------------------

Message: 3
Date: Fri, 23 May 2014 10:55:57 +0200
From: Lo?c Correnson <loic.correnson at cea.fr>
To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
Subject: Re: [Frama-c-discuss] Frama-c and SystemC
Message-ID: <3BDBBB6E-4E84-4A3D-94EE-E04D2AE65E43 at cea.fr>
Content-Type: text/plain; charset="windows-1252"

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.html>

------------------------------

Subject: Digest Footer

_______________________________________________
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

------------------------------

End of Frama-c-discuss Digest, Vol 72, Issue 10
***********************************************

Frama-C-discuss mailing list archives

[Frama-c-discuss] SystemC and time-reliated infromal requirements.