--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Oracles of Jessie tests in source distributions



Hello everybody,

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.

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 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?
- 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)?
- 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.

Note: due to to-be-solved technical difficulties I have not yet
succeeded in compiling and testing any distribution.

Kind regards,
Markus Wagner