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