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 (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>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

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 than the one generated by Frama-C's configure in ptests/.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>