--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on February 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] CHAR_BIT != 8



On 6 February 2012 16:36, Pascal Cuoq <pascal.cuoq at gmail.com> wrote:

> On Mon, Feb 6, 2012 at 2:59 PM, Ned <ned at tropic.org.uk> wrote:
>>
>> I'm interested in using frama-c with a couple of architectures with
>> CHAR_BIT being some value other than 8 (16 in one case, 24 in another).
[..]
> Since your interest in unusual CHAR_BITs presumably stems from your having
> at hand processors with these characteristics, and C compilers for these
> processors, you may be able to discover bugs following the recipes described
> in http://blog.frama-c.com/public/csmith.pdf

Thanks for the reply, Pascal.  In short, I will have to get my hands
dirty:)  I do indeed have compilers for these processors; partly, my
motivation for using Frama-C is as an oracle for CSmith testing of
those compilers - or if not an oracle, at least a second opinion!  At
the moment we're using CSmith to compare different optimisation levels
using a single compiler and to find compiler crashes, but we'd like a
second implementation to compare against.

I think we could use the recipes you describe to bootstrap this.

If we get anywhere I'll post back with results!

Thanks,
Ned.