--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on December 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] another question about ptest.byte



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>