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-discuss Digest, Vol 36, Issue 6

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 36, Issue 6
  • From: florent.garnier at gmail.com (florent garnier)
  • Date: Tue, 10 May 2011 12:05:25 +0200
  • In-reply-to: <mailman.55.1304762445.16842.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.55.1304762445.16842.frama-c-discuss@lists.gforge.inria.fr>
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>