On Mon, Sep 12, 2011 at 3:40 PM, Paulo J. Matos <Paulo.Matos@csr.com>
Thanks for your analysis on the file I sent. I will take a look at it now. By the way? Is the analysis you made to check definedness something I can to on my end?
It will be made available in the new release
Is it a special option to frama-c? Is this similar to C-semantics (http://code.google.com/p/c-semantics/)?
There will be in the next release a number of tweaks
to obtain best results for this use.
I will describe the new options in a blog post at
about the same time as the release.
What prevents from using the previous release
is not so much that these options
are missing, but that a lot of Frama-C front-end and
analysis bugs have been fixed thanks to Csmith
since February, and you would be running into
these same bugs again if you used the
Compared from C-semantics, the projects
started with different objectives, but products of
both projects have been safe interpreters for C
that are supposed to tell if a deterministic,
completely available C program exhibits
any of a large class of unspecified and
undefined behaviors. Functionally, when used for
the purpose of verifying Csmith programs, the
interpreters are comparable.