--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on June 2012 ---
[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