--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] <CAA1cxuiRnanxWHJHhXFpRV9G3+pwnFbnNG9zQrCsx3PHQq+fdA@mail.gmail.com>



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