--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on April 2012 ---
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