--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on December 2011 ---
Just to complete what Pascal just said: - You can add some comment in the DONTRUN: line, e.g. to indicate the name of the master file that is supposed to trigger the test - the configuration of ptests can be altered by a ptests_local_config.ml file: if ptests.byte is launched in a directory which contains ptests_local_config.cmo, it will dynamically load this file. In particular, if you're including Frama-C's Makefile.plugin in your own Makefile and have set the appropriate variables (namely PLUGIN_TESTS_DIRS, possibly PLUGIN_TESTS_LIBS), make ptests_local_config.cmo should create an appropriate configuration. Best regards, -- E tutto per oggi, a la prossima volta Virgile ________________________________ De : frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de Pascal Cuoq [pascal.cuoq at gmail.com] Date d'envoi : lundi 19 d?cembre 2011 11:47 ? : Frama-C public discussion Objet : Re: [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<mailto: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<http://ptests_config.ml> than the one generated by Frama-C's configure in ptests/. Pascal -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? nettoy?e... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20111219/df4612c3/attachment.htm>