--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on July 2009 ---
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