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

  • Subject: [Frama-c-discuss] Oracles of Jessie tests in source distributions
  • From: wagnermar at uni-koblenz.de (Markus Wagner)
  • Date: Thu, 30 Jul 2009 14:25:47 +0200
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