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] [Value analysis] Validating a function with behavior spec.

  • Subject: [Frama-c-discuss] [Value analysis] Validating a function with behavior spec.
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Fri, 13 Apr 2012 11:03:47 +0200
  • In-reply-to: <CAFaEDLCHYJtescjnsqs6gE5q_Nx5+CWSg_3AD=f9pN_AHhq4=w@mail.gmail.com>
  • References: <CAFaEDLCHYJtescjnsqs6gE5q_Nx5+CWSg_3AD=f9pN_AHhq4=w@mail.gmail.com>
On Fri, Apr 13, 2012 at 10:51 AM, sylvain nahas
<sylvain.nahas at googlemail.com> wrote:
> Hi,
>
> I can not validate the somewhat trivial code below

_____

I still remember a guy sitting on a couch, thinking very hard,
and another guy standing in front of him, saying, "And therefore
such-and-such is true".
"Why is that?" the guy on the couch asks.
"It's trivial! It's trivial!" the standing guy says, and he rapidly
reels off a series of logical steps: "First you assume thus-and-so,
then we have Kerchoff 's this-and-that; then there's Waffenstof-
fer's Theorem, and we substitute this and construct that. Now
you put the vector which goes around here and then thus-and-
so..." The guy on the couch is struggling to understand all this
stuff, which goes on at a high speed for about fifteen minutes!
Finally the standing guy comes out the other end, and the guy
on the couch says, "Yeah, yeah. It's trivial."
We physicists were laughing, trying to figure them out. We de-
cided that "trivial" means "proved". So we joked with the math-
ematicians: "We have a new theorem- that mathematicians can
prove only trivial theorems, because every theorem that's proved
is trivial".
_____         Richard P. Feynman


You are complaining that something is not proved.
Fair enough, but if it is not proved it is not trivial.

To answer your question, you cannot prove the kind of functional
property you desire with the value analysis. On the other hand,
for your example, either Jessie or Wp look like they have a good
chance.

Pascal