--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on December 2011 ---
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>