--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on October 2010 ---
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