--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on April 2012 ---
> 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? The value analysis wouldn't work as a C interpreter on Csmith-generated programs if it did not know how to handle casts such as (unit8), because there are a lot of those in Csmith-generated programs (http://blog.frama-c.com/index.php?post/2011/08/29/CompCert-gets-a-safe-interpreter-mode ) 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. Boris Yakobowski has more to say about the provability of the assertions in the original example. I will let him make that other point. Pascal