--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on September 2013 ---
? 2013/9/3 15:23, 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. Re: How to use the frama-c builtins programmatically? (David) > 2. Re: How to use the frama-c builtins programmatically? > (Virgile Prevosto) > 3. Re: installation on Ubuntu (Jorge Adriano Branco Aires) > 4. Re: How to use the frama-c builtins programmatically? (David Yang) > 5. Re: How to use the frama-c builtins programmatically? > (Virgile Prevosto) > 6. JFLA 2014 - Troisieme appel a Communication (Christine Tasson) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Mon, 02 Sep 2013 20:00:25 +0800 > From: David <abiao.yang at gmail.com> > To: frama-c-discuss at lists.gforge.inria.fr > Subject: Re: [Frama-c-discuss] How to use the frama-c builtins > programmatically? > Message-ID: <52247DD9.3080407 at gmail.com> > Content-Type: text/plain; charset=UTF-8; format=flowed > > ? 2013/9/2 16:56, frama-c-discuss-request at lists.gforge.inria.fr ??: >> I think there is some misunderstanding here. When you add >> /usr/local/share/frama-c/libc/fc_runtime.c to the list of source files >> to consider, all C implementations present in this file will be >> treated as C functions to be analyzed, exactly that the functions that >> are defined in file.c Value analysis built-in mechanism allows to >> replace the normal analysis of a C function by a call to an OCaml >> function which operates directly to the internal states of Value >> analysis, simulating the behavior of the corresponding C function. >> These two behaviors are completely different. What are you trying to >> achieve? > Dear Virgile, > > Thank you for replying me promptly. > I am trying to treat those C functions in fc_runtime.c to be analyzed. > I can ahieve this by codeing like this: > > Kernel.Files.add "/usr/local/share/frama-c/libc/fc_runtime.c"; > > Thanks again. > > David > > > > > > ------------------------------ > > Message: 2 > Date: Mon, 2 Sep 2013 15:05:10 +0200 > From: Virgile Prevosto <virgile.prevosto at m4x.org> > To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> > Subject: Re: [Frama-c-discuss] How to use the frama-c builtins > programmatically? > Message-ID: > <CA+yPOVgfNZj49+J2dLYRDJHzkUOKPv41PiT39vMtJaec8GS5kA at mail.gmail.com> > Content-Type: text/plain; charset=ISO-8859-1 > > 2013/9/2 David <abiao.yang at gmail.com>: > >> I am trying to treat those C functions in fc_runtime.c to be analyzed. >> I can ahieve this by codeing like this: >> >> Kernel.Files.add "/usr/local/share/frama-c/libc/fc_runtime.c"; >> > Yes, then it's the best way to achieve what you want. For portability, > if you use your script on different machines where Frama-C might not > always be installed on /usr/local, you can use something like > (Config.datadir ^ "/libc/fc_runtime.c"), but it really depends on your > configuration. > > Best regards, Sorry this is a test on how to reply without opening a new topic.