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

[Frama-c-discuss] Frama-c-discuss Digest, Vol 36, Issue 6



2011/5/7 <frama-c-discuss-request at lists.gforge.inria.fr>

> 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. Value analysis : How to use the value analysis plugin from
>      another one ? (florent garnier)
>   2. Re: Value analysis : How to use the value analysis plugin
>      from another one ? (Anne Pacalet)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Fri, 6 May 2011 15:44:01 +0200
> From: florent garnier <florent.garnier at gmail.com>
> Subject: [Frama-c-discuss] Value analysis : How to use the value
>        analysis plugin from another one ?
> To: frama-c-discuss at lists.gforge.inria.fr
> Message-ID: <BANLkTi=3oRHSMrBCof3wMam3K3zPKaVeug at mail.gmail.com>
> Content-Type: text/plain; charset="iso-8859-1"
>
> Hi,
>  Maxime Gaudin and I are currently developing a Frama-c plugin,
> which aims to generate some abstraction of C functions. We would
> like to call the value analysis plugin from ours, in order to have
> some information about the ranges of some variables at some given
> location.
>
> We tried to use the Db.Value.access function, just like presented in the
> Chapter
> 3 of the value analysis manual, as well as others. Unfortunately we
> got stuck at the compilation stage, he we have some difficulties to
> find out the proper way to do it.
>
> Does somebody have some examples that show how to call the value analysis
> plugin from another one ?
>
> Thanks in advance,
>  Florent and Maxime.
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <
> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110506/a9093594/attachment-0001.htm
> >
>
> ------------------------------
>
> Message: 2
> Date: Fri, 06 May 2011 16:04:39 +0200
> From: Anne Pacalet <anne.pacalet at inria.fr>
> Subject: Re: [Frama-c-discuss] Value analysis : How to use the value
>        analysis plugin from another one ?
> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr>
> Message-ID: <4DC3FFF7.6090607 at inria.fr>
> Content-Type: text/plain; charset=ISO-8859-1; format=flowed
>
> Le 06/05/2011 15:44, florent garnier a ?crit :
> > Does somebody have some examples that show how to call the value analysis
> > plugin from another one ?
>
> You can have a look at the PDG plug-in for instance.
> In [build.ml] it calls :
>
>   if not (Db.Value.is_computed ()) then !Db.Value.compute ();
>
> I am not absolutly sure that this is the right way of doing it,
> but it works.
>
> If you have some compilation problems, maybe giving the error message
> would help us to help you.
>
> Hope this help.
> --
> Anne.
>
>
>
> ------------------------------
>
> _______________________________________________
> 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 36, Issue 6
>

 Thank you Anne for your fast and useful answer. Maxime and I made some
progress,
 and we reached the situation described below :

We  can now :
 _ Initialize the value analysis using the functions you were speaking about
in your previous mail,
_ We can pretty print those information using the API pretty printer, for
any lvalue at any
location.

At a glance, we get some results which type is Cvalue_type.V and that
encodes ranges
of values, however we have no clue about how to get the information that
follow :

-> Gettng the infimum and the supremum bounds of this range of values.
-> Getting the set of the elements whenever it is possible.

Can somebody tip us about those issues ?
Thanks in advance,
 Maxime and Florent.


ps : Here is the original mail from Maxime, written in French.

Bonjour,
Apr?s plusieurs jours de travail, Florent Garnier et moi m?me sommes parvenu
? :
- Initialiser correctement l'analyse des valeurs
- Effectuer un *pretty**print* de celles-ci
- Choisir l'endroit dans le code o? nous d?sirons analyser une lvalue

Autrement dit, nous nous retrouvons avec une structure du type de retour de
*Db.Value.access*, *i.e. Cvalue_type.V*. Ce type code des intervalles de
valeurs mais nous ne parvenons pas ? acc?der ? :
- L'ensemble des ?l?ments de l'intervalle
- Le plus petit ?l?ment
- Le plus grand

Merci de votre aide,

*Maxime GAUDIN*

*El?ve ing?nieur ? l'INSA Lyon, 4?me ann?e,*

*D?partement informatique*
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20110510/dcfaae0e/attachment.htm>