--- layout: fc_discuss_archives title: Message 12 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,

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.

The tests are located in a directory under
~/frama-c-Nitrogen-20111001/tests, they have run.config comments as
explained in 5.5.2, and I use ptests as explained in example 5.7.

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.

My .cm[i|o|xs]-files are in my source directory and symlinked
from /usr/local/lib/frama-c/plugins. Only the cmxs-file is executable,
not cm[i|o], which is different from the permissions of the other files
in /usr/local/lib/frama-c/plugins.
-- 
Best regards,
Boris