--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on May 2011 ---
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>