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

  • Subject: [Frama-c-discuss] Problem with ptests
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Fri, 22 Jun 2012 13:13:39 +0200
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