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] proving false and counter examples

  • Subject: [Frama-c-discuss] proving false and counter examples
  • From: tomahawkins at gmail.com (Tom Hawkins)
  • Date: Sat, 8 May 2010 12:10:17 -0500
I was reading the FAQ on the Frama-C wiki on the semantics of the gWhy
icons.  I found this statement a little surprising:

"invalid (red dot): the VC is not a true formula. In principle,
invalid should be identified with unknown, because provers can very
rarely say that a formula is definitely not true. Historically,
Simplify answers is either valid or invalid, where invalid indeed
means unknown. The GWhy maps those invalid to the question mark but
the textual output might still classified them as invalid."

In the test cases I have run on Jessie till this point, I've never
seen a red dot; just timeouts (scissors) or unknowns (question mark).
And even for examples I would think would be trivial to proof false,
like this:

  //@ ensures \result;
  int f() {return 0;}

Why is it difficult to determine if a formula is false?  I am used to
model checking, where conclusive false results are common, as are
counter examples, which greatly aid the debug process.  When gWhy
gives me a scissors, without a counter example, I'm kind of left in
the dark.  This is not meant to be a criticism.  I just don't
understand the limitations of this logical framework yet.

-Tom