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

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



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>