--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on April 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Value analysis] Validating a function with behavior spec.



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