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 and termination

  • Subject: [Frama-c-discuss] Value analysis and termination
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Tue, 12 Oct 2010 07:48:56 +0200
  • In-reply-to: <1286823000.2466.79.camel@iti27>
  • References: <1286823000.2466.79.camel@iti27>
Hello,

On Mon, Oct 11, 2010 at 8:50 PM, Boris Hollas
<hollas at informatik.htw-dresden.de> wrote:
> However, the value analysis shows i \in {-4,0,4} at this point. But i ==
> 0 is not possible since !(i % 2 == 0) is necessary for the loop to
> terminate. ?Why doesn't the value analysis detect this?

It comes down to the fact that the following piece of program
  if (i % C1 == C2) { ... }
does not reduce the value of i in the "then" branch.

It could, of course. I will see if a pattern can be added easily for
this construction. But there is no limit to the number of
constructions for which something smart could be done. You have to
stop somewhere.

Pascal