--- layout: fc_discuss_archives title: Message 40 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:21 AM, Pascal Cuoq wrote:
>> The imprecise operation here is == between non-singleton sets of
>> values. val can be 1 or 2, and retval can be 1 or 2, therefore the
>> equality may be true but cannot be guaranteed to be so.

Ok, you're saying that the value analysis does not have relational 
domains. I had forgotten that. thanks

-- 
Yannick Moy, Senior Software Engineer, AdaCore