On Sun, Jul 31, 2011 at 11:37 AM, Xavier Leroy
<Xavier.Leroy@inria.fr> wrote:
Dear Csmith developers,
[ A bit of background: this is the CompCert guy (Xavier Leroy)
speaking. I've been playing with Csmith this afternoon, with the idea
of using it to test a reference interpreter for CompCert C's formal
semantics, just like Rosu, Ellison and you have been doing with the
kcc reference interpreter. My reference interpreter is not yet 100%
up to the task, but I'm getting interesting feedback already from
Csmith-generated examples. In the process, I found a few unexpected
behaviors of Csmith that I'm taking the liberty to report, in separate
messages. Here is unexpected behavior #1. ]
When run with option --check-global, Csmith produces a "main" function
that has no "return" at the end. E.g. with --seed 123:
int main (int argc, char* argv[])
{
func_1();
printf("checksum g_2 = %d\n", g_2);
printf("checksum g_3 = %d\n", g_3);
}
This is undefined behavior and my reference interpreter balks at it.
Could you just add "return 0;" at the end? Thanks,
- Xavier