--- layout: fc_discuss_archives title: Message 38 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.



> 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