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] another question about ptest.byte

  • Subject: [Frama-c-discuss] another question about ptest.byte
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Mon, 19 Dec 2011 11:47:05 +0100
  • In-reply-to: <569C6D7D26484241A530B87F45ADE1F8820BF3@AOFRWMBXRSC004.resources.atosorigin.local>
  • References: <569C6D7D26484241A530B87F45ADE1F8820BF3@AOFRWMBXRSC004.resources.atosorigin.local>
Hello St?phane,

On Mon, Dec 19, 2011 at 11:30 AM, DUPRAT Stephane
<stephane.duprat at atos.net>wrote:

> The question is about tests with multiple files. In first use of ptest, a
> test is identified by a sourcefile. But is it possible to make a test with
> several files in the same Frama-C session ?
>

Yes. The directory tests/idct contains such a test: the files
ieee_1180_1990.c and idct.c only make sense when analyzed together. In
order to do this, idct.c contains:
/* run.config
   DONTRUN:
*/

and ieee_1180_1990.c contains:
/* run.config
   OPT: -float-normal -val -deps -out -input tests/idct/idct.c share/math.c
-journal-disable -remove-redundant-alarms
*/

in which "tests/idct/idct.c" is the important part for you.

>
> The remark is about a message error that I have when I launch ptest.byte
> without arguments:
> >$ ptests.byte
> >Fatal error: exception Sys_error("tests/idct: Not a directory")
>
> In my configuration, I have a directory named tests in which I have a
> subdir for each familiy tests.
> And for example, "ptests.byte test_XX" is working well.
>

People who use ptests outside of its normal context provide a different
ptests_config.ml than the one generated by Frama-C's configure in ptests/.

Pascal
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111219/4a9687ea/attachment.htm>