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] Oracles of Jessie tests in source distributions

Hi!

> Regarding the source distributions of Lithium and Beryllium, I noticed
> that there are quite a lot of tests included. But the folders "oracle"
> and "result" seem to be empty by default.

Results are generated from your compiled version. Oracles should
arguably be distributed, but aren't. We do not distribute them because
we were not sure they were completely platform-independent (including
such meaningless information as the name of temporary files,
or depending on the host system's headers).
Making sure they are clean and distributing them is on our to-do list.

> Especially for the tests of the verification plug-in Jessie, I would
> like to know where the oracles come from. I am a little confused right
> now and I would be very happy if someone could shed light on this.

The oracles are generated by the target "oracles" in the Makefile
once Frama-C is compiled. You have to type "make oracles",
it is not done as part of the compilation. Sorry if
http://frama-c.cea.fr/install_beryllium.html
is not clear enough on this topic.
The only purpose that the distributed tests can satisfy, since
we do not distribute the oracles, is that if you wanted to modify
Frama-C yourself, you could use the tests to check that everything
else is still working as it did before the patch.

> The compilation instructions indicate that the oracles are set up
> automatically. Well, I wonder right now how that is done.
> - Do you assume that all the test cases are correct, i.e., the  
> programs
> fulfill the specifications? --> Are there negative test cases as well?

All plug-ins should include negative tests, however human nature being
what it is, there certainly aren't nearly enough. Especially not
if these tests were supposed to give the user confidence in the tool,
in which case negative tests would be the most important.

If you need to trust Frama-C as part of a certified verification
process, the first step is to write additional tests for your
own evaluation, and then quite a bit more for your certification
authority.

> - So you set up the oracles by running them and recording the results
> "as oracles" and later you run tests and compare the observed results
> with earlier version of the runs (i.e. the oracles)?

This is how it happens for the distributed version. For the development
version, the oracles are part of the SVN.

> - My understanding so far was that the oracle for "does the function
> fulfill its specification" is provided by a human or by another
> verification engine.

The oracle is provided by a human, specifically, the developer who
committed the oracle file to the SVN. Again, we are sorry for the
inconvenience caused by us not distributing oracles files.

Pascal