[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [csmith-dev] compcert support
On 11/08/11 05:02, John Regehr wrote:
I should add that I've been doing some CompCert testing lately w/o the
special --ccomp flag to Csmith and it works fine. It seems that many
CompCert limitations have disappeared in the last year or two. I was
thinking about pulling all of the CompCert-specific code out of Csmith.
This might be a good opportunity for me to point out some work I've been
doing recently on an executable version of the CompCert C semantics.
This provides a single-step function in CIC which (with the exception of
some "external" functions) matches the existing CompCert C semantics.
More interesting for Csmith is the OCaml driver which runs the program
using this function until it completes or gets stuck (a little like kcc,
but specialized to CompCert C).
Using it with Csmith doesn't generate too many surprises (the problems
are mostly to do with features not supported by CompCert C, such as
structure passing). There was an interesting bug in the compiler with
the evaluation of conditional expressions that will be fixed in the next
CompCert release - but it was encountered in the safe_math.h functions
rather than the random code!
One Csmith feature that would be useful for testing this sort of thing
would be options to turn off struct/union assignments, and structs on
the left side of a comma operator. I've had to turn comma off entirely
because CompCert doesn't support structs on the left side.
If anyone is interested in the semantics, they can be found at the
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.