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] Problem with ptests

Hello Boris,

2012/6/22 Boris Hollas <hollas at informatik.htw-dresden.de>:

> today, I've discovered that all my regression tests succeed because the
> result logs just contain an invariant error message that my plug-in is
> not known. However, frama-c -help does list my plug-in and it works as
> expected if I specify exactly the same command line options as in OPT in
> the test file's run.config.

Did you launch the tests with make tests or directly with ptests.byte?
In the latter case, you might need to generate ptests_local_config.cmo
in the main directory of your plug-in
(if you have a Makefile that includes Makefile.dynamic, simply make
ptests_local_config.cmo. make tests does that implicitly, so that you
don't need this step).
If ptests_local_config.cmo does exists and the issue persists, we'll
need to know more about your set-up:
- Do you compile the plug-in against an installed version of Frama-C,
or together with the Frama-C sources themselves?
- Which steps do you perform for launching the tests?
- What is the output of ptests.byte -show tests/$MY_PLUGIN/$SOME_TEST.c?

> I've initialized the tests by creating directories oracle and result in
> my plug-in's test directory (as ptests doesn't seem to create these on
> its own) and I've run ./bin/ptests.byte -update <plug-in>. Subsequent
> runs of ptests report OK for everything, even if I introduce syntax
> errors in the .c test-files.

Usually (after ptests_local_config.cmo is generated), it's a good idea
to use ptests.byte -show before -update, to ensure that the oracle
will be meaningful.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile