--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on April 2012 ---
On 04/13/2012 11:03 AM, Pascal Cuoq wrote: > 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, just to satisfy my curiosity, what is causing imprecisions in the value analysis in the code: retval = (uint8)val; /*@ assert retval == val; */ Is it the cast which is treated as an unknown function? Then its transition function could be modeled more precisely I guess, which would allow value analysis to prove both assertions, right? What about the postconditions, would value analysis be able to prove them? I guess it could if you analyze each behavior separately (otherwise you'd need a disjunctive domain), maybe that's what you do already? -- Yannick Moy, Senior Software Engineer, AdaCore