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] <CAA1cxuiRnanxWHJHhXFpRV9G3+pwnFbnNG9zQrCsx3PHQq+fdA@mail.gmail.com>

  • Subject: [Frama-c-discuss] <CAA1cxuiRnanxWHJHhXFpRV9G3+pwnFbnNG9zQrCsx3PHQq+fdA@mail.gmail.com>
  • From: abiao.yang at gmail.com (David)
  • Date: Wed, 04 Sep 2013 02:33:46 +0800
  • In-reply-to: <mailman.5305.1378193008.1217.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.5305.1378193008.1217.frama-c-discuss@lists.gforge.inria.fr>
? 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.