For years now I have been successfully building CompCert in cygwin, but now I have a problem.

In the last line of Makefile.extr,
echo $(OCAMLDEP) $(foreach d,$(DIRS),$(wildcard $(d)/*.mli $(d)/*.ml)) $(GENERATED) >.depend.extr || { rm -f .depend.extr; exit 2; }

the arguments to the "echo" command are 8487 characters long (in JH Jourdan's port of CompCert to Coq 8.5). The "make" program in cygwin seems to have an internal limit of 8176 characters for a single line (e.g., the result of the $(foreach...)). This is not the ARG_MAX limit to the exec system call, which is 32000 on cygwin; it's something internal to "make".

My workaround is:

depend: $(GENERATED)
    @echo "Analyzing OCaml dependencies"
    # The next few lines are to work around an internal line-length limit in the cygwin build of 'make'
    @echo >.depend.extr1 $(OCAMLDEP)
    @echo >>.depend.extr1 $(foreach d,$(DIRS),$(wildcard $(d)/*.mli))
    @echo >>.depend.extr1 $(foreach d,$(DIRS),$(wildcard $(d)/*.ml))
    @echo >>.depend.extr1 $(GENERATED)
    @echo >>.depend.extr1 '>.depend.extr'
    tr '\n' ' ' <.depend.extr1 >.depend.extr2
    sh -c ./.depend.extr2 || { rm -f .depend.extr; exit 2; }
    rm -f .depend.extr1 .depend.extr2

I have found a minor omission in the way compcert dumps its rtl tree.
Obviously it is not very nice to find bad operators being dumped for
supposedly validating translations of a source code. I am sure you will
have no difficulty reproducing the problem, but if necessary I can send a test case.

jrrk2@serenity CompCert-2.6]$ diff -u ia32/PrintOp.ml{,}
--- ia32/PrintOp.ml 2015-12-21 09:09:21.000000000 +0000
+++ ia32/PrintOp.ml 2016-01-08 12:11:45.160542829 +0000
@@ -119,6 +119,9 @@
| Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2
| Olowlong, [r1] -> fprintf pp "lowlong(%a)" reg r1
| Ohighlong, [r1] -> fprintf pp "highlong(%a)" reg r1

• | Onot, [r1] -> fprintf pp "not(%a)" reg r1
• | Omulhs, [r1;r2] -> fprintf pp "mulhs(%a,%a)" reg r1 reg r2
• | Omulhu, [r1;r2] -> fprintf pp "mulhu(%a,%a)" reg r1 reg r2
  | Ocmp c, args -> print_condition reg pp (c, args)
  | _ -> fprintf pp ""

[jrrk2@serenity CompCert-2.6]$

(This report is for the struct-passing branch).

fdisk on OpenBSD crashes randomly when compiled with CompCert. I've created a reduced test case:
http://dickman.org/compcert/test24/ccomp/foo.c

The CompCert version alternates between segfaulting and printing 0 instead of the expected AA55:

$ ./gcc/foo
dmbr_sign=AA55
$ ./ccomp/foo
Segmentation fault (core dumped)
$ ./ccomp/foo
dmbr_sign=0

The code in foo.c does the following:

• read the first 512 byte sector (the master boot record) from disk wd0
• memcpy the char* data into a struct dos_mbr
• print out the MBR signature (the last 2 bytes of the MBR).

All gcc and CompCert outputs were saved here:
http://dickman.org/compcert/test24/

The code causes a fatal error due to the use of "inline".

$ cat foo.c
typedef __builtin_va_list va_list;

inline void foo2(const char *f, ...)
{
    va_list args;
    __builtin_va_start((args), f);
}

void foo1(const char *str)
{
    foo2(str, 0);
}

int main() {
    foo1("hi");
}
$ ccomp -fall foo.c
Fatal error: exception Invalid_argument("Fatal error: va_start used in non-vararg function")
Raised at file "pervasives.ml", line 31, characters 25-45
Called from file "ia32/PrintAsm.ml", line 549, characters 4-67
Called from file "ia32/PrintAsm.ml", line 662, characters 6-33
Called from file "list.ml", line 73, characters 12-15
Called from file "ia32/PrintAsm.ml", line 956, characters 2-45
Called from file "list.ml", line 73, characters 12-15
Called from file "ia32/PrintAsm.ml", line 1062, characters 2-50
Called from file "driver/Driver.ml", line 162, characters 2-31
Called from file "driver/Driver.ml", line 258, characters 6-50
Called from file "driver/Driver.ml", line 353, characters 34-40
Called from file "driver/Driver.ml", line 585, characters 22-70
$ gcc -std=c99 -pedantic foo.c
foo.c:4: warning: C99 inline functions are not supported; using GNU89
foo.c:4: warning: to disable this warning use -fgnu89-inline or the gnu_inline function attribute
$

$ ccomp -version
The CompCert C verified compiler, version 2.7.1
$ ccomp -fall small.c
small.c:1: Warning: empty struct.
small.c:7: Error: return value has type struct inode *
instead of the expected type struct inode.
Fatal error: exception File "cparser/StructReturn.ml", line 488, characters 10-16: Assertion failed
Raised at file "cparser/StructReturn.ml", line 488, characters 10-22
Called from file "cparser/StructReturn.ml", line 561, characters 9-69
Called from file "cparser/Transform.ml", line 210, characters 19-33
Called from file "cparser/Parse.ml", line 22, characters 11-157
Called from file "cparser/Parse.ml", line 77, characters 6-59
Called from file "driver/Frontend.ml", line 58, characters 10-59
Called from file "driver/Driver.ml", line 72, characters 12-41
Called from file "driver/Driveraux.ml", line 118, characters 34-40
Called from file "driver/Driver.ml", line 547, characters 22-70
$ cat small.c
struct inode {};
struct afs_vnode {
struct inode vfs_inode;
};
struct inode fn1() {
struct afs_vnode *vnode;
return &vnode->vfs_inode;
}
$

gcc allows this c11 feature as a C extension:

$ cat foo.c
struct T { int tag; union { float x; int n; }; };

int f(){
        struct T var;
        var.x = 3.0;
}
$ gcc -c foo.c
$ gcc -std=c99 -c foo.c
foo.c:1: warning: declaration does not declare anything
foo.c: In function 'f':
foo.c:5: error: 'struct T' has no member named 'x'
$ gcc -std=gnu99 -c foo.c
$

CompCert doesn't currently support this feature:

$ ccomp -fall -c foo.c
foo.c:5: Error: struct 'T' has no member named 'x'.
Fatal error; compilation aborted.
1 error detected.

Here's the gcc documentation:
https://gcc.gnu.org/onlinedocs/gcc/Unnamed-Fields.html

I don't know if this is just a matter of updating the user manual, or if I misunderstood its meaning: section 7.15 says that the va_arg macro cannot fetch composite types, and that a compile-time error is generated if one tries to do so. I tried the following code in IA-32 Linux and it does compile with CompCert 2.4 and 2.5:

#include <stdio.h>
#include <stdarg.h>

typedef struct { int v; float f; } pair;
typedef union { char s[4]; int i; } variant;

void printer (int n, ...) {
  va_list argp;
  va_start(argp, n);
  pair p = va_arg(argp, pair);
  printf("pair = %d, %f\n", p.v, p.f);
  variant v1 = va_arg(argp, variant);
  printf("variant(s) = %s\n", v1.s);
  variant v2 = va_arg(argp, variant);
  printf("variant(i) = %d\n", v2.i);
  va_end(argp);
}

int main() {
  pair p = {42, 3.14};
  variant v1 = {.s = "abc"};
  variant v2 = {.i = 13};
  printer(3, p, v1, v2);
  return 0;
}

When run, it produces nonsensical results by default (like #20), but activating -fstruct-return makes it work without issues (again, like #20). So it seems to me that it is just a matter of updating the user manual.

Bit-field initialization via -fbitfields emulation leads to undefined behavior in most cases. It would be nice to be able to do it without having to resort to a static-storage variable.

For instance, in this program:

typedef struct { int f: 8; } t;
int main() {
    t p = {0};
    return p.f;
}

The compiled code executes as expected, but the emulated bit-fields generate reads from uninitialized variables. Here's an excerpt of the .compcert.c code via -dc:

int main(void)
{
  struct _108 p;
  p.__bf1 = p.__bf1 & ~255U | (unsigned int) 1 << 0U & 255U;
  return (int) (p.__bf1 << 24) >> 24;
}

The only way I was able to initialize it was by introducing a static-storage struct and copying its value:

typedef struct { int f: 8; } t;
t t_zero;
int main() {
    t p = t_zero;
    return p.f;
}

On a side note, the CompCert website (http://compcert.inria.fr/compcert-C.html) mentions that designated initializers are not supported, but they seem to work, at least in expressions such as t p = {.g = 1, .f = 2} and int a[10] = {[4] = 1, [2] = 3}.

For IA32 assembly, it seems that compiling code to a processor not supporting SSE would require mostly (1) rewriting the assembly generation (using non-SSE instructions) and (2) using x87 floating-point registers instead of MMX.

In principle, there seems to be no major hindrance to such effort (other than the fact that it is mostly useless nowadays). Is there any hidden dependency that could prevent that from happening?

When compiling pf.c CompCert runs out of memory. Pre- and post-processed source here:

• http://dickman.org/compcert/2.4/test13/pf.c
• http://dickman.org/compcert/2.4/test13/pf.i

Console output:

$ ccomp pf.i
../../../../sys/lock.h:47: Warning: empty struct.
../../../../net/pf.c:3045: Warning: argument #2 of function call has type
  char * instead of the expected type u_int8_t const *.
../../../../net/pf.c:3046: Warning: argument #2 of function call has type
  char * instead of the expected type u_int8_t const *.
../../../../net/pf.c:3050: Warning: argument #2 of function call has type
  char * instead of the expected type u_int8_t const *.
../../../../net/pf.c:3051: Warning: argument #2 of function call has type
  char * instead of the expected type u_int8_t const *.
../../../../net/pf.c:3056: Warning: argument #2 of function call has type
  char * instead of the expected type u_int8_t const *.
../../../../net/pf.c:3057: Warning: argument #2 of function call has type
  char * instead of the expected type u_int8_t const *.
Fatal error: out of memory.

CompCert does not compile this code, with the error message Initializer is not a compile-time constant (undefined binary operation):

int a;
unsigned long b[] = {(unsigned long)&a+1};

Both GCC and Clang do accept it without warnings.

It seems to me that GCC and Clang's behaviors are unsafe, but I'd like to confirm anyway whether it is expected that CompCert might accept such code in the future.

I couldn't find the CompCert user manual (http://compcert.inria.fr/man/) on Github, neither on the .tgz archives. There's the 2.4 release on HAL (https://hal.inria.fr/hal-01091802) and the latest one (currently 2.5) on the website, but is there an archive where older versions could be found? For instance, like OCaml's documentation which has the standard URL pointing to the latest release and alternative URLs pointing to fixed versions. This is mainly for future referencing purposes.

A user reports an assembler error on MacOS X Yosemite:

../../ccomp -stdlib ../../runtime -dparse -dc -dclight -dasm -fall -o int32.compcert int32.c
[...]
int32.s:562:Unknown pseudo-op: .global
int32.s:562:Rest of line ignored. 1st junk character valued 95 (_).
Error during assembling.

It works with ".globl" instead of ".global". See: http://stackoverflow.com/questions/10512248/unknown-pseudo-op-global

In the CompCert 2.6 distribution, "Note 2" seems to be inaccurate.

It says, 'If Menhir answers "-package menhirLib", then Menhir was installed with ocamlfind...'
But in fact, I installed my menhir-20151112 without ocamlfind, without opam,
and yet when I run
menhir --table --suggest-comp-flags
the response is
-package menhirLib
which contradicts the sentence in the Makefile.menhir.

You might wonder why I installed menhir this way; well, I'm using a shared Linux server on which I don't have root privileges.

So I had to fix the problem by editing Makefile.menhir to set the MENHIR_INCLUDES to
the particular path on my machine.

From the LICENSE file, lines 74-76:

The files contained in the runtime/ directory and its subdirectories are Copyright 2013-2014 INRIA and distributed under the terms of the BSD license, included below.

As far as I can see, only the following licenses follow:

• INRIA Non-Commercial License Agreement for the CompCert verified compiler
• GNU General Public License, version 2
• GNU Lesser General Public License, version 3

Inclusion of this particular license is quite important, because there are at least three well-known variants of it.

See below for what looks like an internal error.

$ cat foo.c
typedef struct _S S;

struct _S {
    int header;

    struct {
        double value;
    } values[10];

};

void foo() {
    int x;

    S event = {
            .header = 0,
    };
}
$ gcc -std=c99 -pedantic -c foo.c
$ gcc -c foo.c
$ ccomp -fall -c foo.c
Fatal error: exception Env.Error(_)
Raised at file "cparser/Env.ml", line 184, characters 9-48
Called from file "cparser/Cutil.ml", line 873, characters 15-37
Called from file "cparser/Unblock.ml", line 40, characters 21-44
Called from file "list.ml", line 89, characters 16-37
Called from file "cparser/Unblock.ml", line 192, characters 14-76
Called from file "cparser/Unblock.ml", line 233, characters 29-51
Called from file "cparser/Unblock.ml", line 241, characters 13-39
Called from file "cparser/Unblock.ml", line 274, characters 19-39
Called from file "cparser/Parse.ml", line 26, characters 2-36
Called from file "cparser/Parse.ml", line 60, characters 6-54
Called from file "driver/Driver.ml", line 99, characters 10-59
Called from file "driver/Driver.ml", line 168, characters 27-58
Called from file "driver/Driver.ml", line 353, characters 34-40
Called from file "driver/Driver.ml", line 585, characters 22-70

The following command line fails:

$ ccomp -Wl,shared -o libwhatever.so.1.1 X.so Y.so
Unknown argument `X.so'

Renaming *.so to *.o works fine:

$ ccomp -Wl,shared -o libwhatever.so.1.1 X.o Y.o
$

gcc works with both cases.

Could you please detail what parts of multi-byte characters are supported by CompCert? Or, inversely, if there are specific multi-byte-related features which are not supported?

In particular, some compilers accept this code (e.g. GCC, Clang), while CompCert emits a warning (escape sequence is out of range (code 0x3B1)) and then crashes:

#include <stdio.h>
int main() {
  printf("\u03B1-conversion\n");
}

Also, whenever a wide character literal is used in a function such as wprintf, a warning similar to argument #1 of function call has type int * instead of the expected type wchar_t const * is emitted. This seems to impact the result of this function, which differs from GCC/Clang in examples such as:

#include <stdio.h>
#include <wchar.h>
#include <locale.h>

int main() {
  setlocale(LC_ALL, "en_US.UTF-8");
  wchar_t c = L'\x3b1';
  wprintf(L"α %lc\n", c);
}

CompCert prints some nonsensical values such as α ? instead of α α.

After searching a bit, I didn't find any proven implementations of loop unrolling in CompCert.

Are there any such implementations that you are aware of? Otherwise, is it too complicated to be done (say, in a few days)?

If there are none, I'd like to try doing it, but I'm afraid it has already been tried and the proof would require several days/weeks of extensive work. I'd wager it's not complex enough to justify an article, but not simple enough to be done "for fun".

It seems that RTLgen would be the best place to do it, but defining the measure over CminorSel states with unrolling seems complicated.

CompCert seems to have a difference in behaviour from gcc when either the prototype or the function definition is declared static, but not both. Here's an example with foo.c and bar.c:

# cat foo.c
static int foo(void);

int foo(void) {
        return 1;
}
# cat bar.c
int foo(void);

static int foo(void) {
        return 1;
}
# gcc -c foo.c
# gcc -c bar.c
bar.c:3: error: static declaration of 'foo' follows non-static declaration
bar.c:1: error: previous declaration of 'foo' was here
# ccomp -fall -c foo.c
foo.c:3: Warning: redefinition of 'foo' with incompatible storage class.
# ccomp -fall -c bar.c
bar.c:3: Warning: redefinition of 'foo' with incompatible storage class.

I believe CompCert should not show a warning with foo.c and should fail to compile bar.c as gcc does. Here's a stackoverflow link where someone references the C standard:

http://stackoverflow.com/questions/15670010/does-a-static-function-need-the-static-keyword-for-the-prototype-in-c

The following test case causes CompCert 2.7 to have a fatal error:

$ ccomp-2.7 small.c
Fatal error: exception File "ia32/Asmexpand.ml", line 190, characters 5-11: Assertion failed
...
$
$ cat small.c
volatile long long a;
unsigned b;

int main ()
{
a = b;
return 0;
}
$

As a followup to issue #6:

$ cat foo.c
#include <wchar.h>

int main() {
        wcschr(L"abcd", L'c');
}
$ ccomp -fall foo.c
foo.c:4: Unsupported feature: wide string literal

I think somewhere between commits a4b766..3b8a09. the regress tests might have broken down:

gmake[1]: Entering directory '/home/ports/pobj/compcert-2.4.13/compcert-2.4.13/test/regression'
[...snip...]
../../ccomp -stdlib ../../runtime -dparse -dc -dclight -dasm -fall -o compound.compcert compound.c -lm
compound.c:31: Error: incomplete type char[].
compound.c:37: Error: incomplete type int const[].
compound.c:76: Error: incomplete type char *[].
compound.c:136: Error: incomplete type int[].
4 errors detected.
Makefile:49: recipe for target 'compound.compcert' failed

gcc allows basic asm blocks outside of any function:

$ cat foo.c
asm("cli");
int main() { return 1; }
$ gcc foo.c

compcert, doesn't seem to support this:

$ ccomp -finline-asm foo.c
foo.c:1: syntax error.
Fatal error; compilation aborted.
1 error detected.

gcc is able to compile an empty switch statement but compcert does not seem to be able to.

$ cat foo.c
int main() {
    int i = 0;
    switch(i) {
    }
}
$ cc -std=c89 -pedantic foo.c
$ cc -std=c99 -pedantic foo.c
$ ccomp -fall foo.c
foo.c:3: Unsupported feature: ill-formed 'switch' statement
$

I've reverted commit 334be23 on my end (the fix for issue #14). It seems to break my build as in this example below:

$ ccomp -I/usr/src/lib/csu/i386 -I/usr/src/libexec/ld.so -I/usr/src/libexec/ld.so/i386 -c /usr/src/lib/csu/crt0.c
In file included from /usr/src/lib/csu/crt0.c:39:
/usr/src/lib/csu/boot.h:48:18: error: path.h: No such file or directory
/usr/src/lib/csu/boot.h:49:21: error: resolve.h: No such file or directory
/usr/src/lib/csu/boot.h:50:17: error: sod.h: No such file or directory
/usr/src/lib/csu/boot.h:52:24: error: dl_prebind.h: No such file or directory
Error during preprocessing.
$
$ ls /usr/src/libexec/ld.so/path.h
/usr/src/libexec/ld.so/path.h

I suspect it's because the directory is called ld.so.

Please add cparser/Parser.v (and any other output of menhir) to the cparser directory of the repo,
and adjust the "configure" and "Makefile" so that menhir is not required for ordinary installation.

Right now, an ordinary user wanting to install CompCert from github
faces this problem:

CompCert requires menhir 20151112 (last year's version won't suffice).
Menhir 20151112 requires ocaml 4.02 (version 4.01 won't suffice).
This is getting painful. It would be easier if Parser.v was committed
to the git repo in addition to Parser.vy, so that only those users who
wanted to edit Parser.vy would have to install menhir. I imagine
the rest of CompCert will build just fine on ocaml 4.01. (This was
certainly true in CompCert 2.5)

It seems that ./configure always checks for the system version of Coq, although the makefile uses the COQBIN prefix:

$ $COQBIN/coqc -v
The Coq Proof Assistant, version 8.4pl6 (May 2016)
compiled on May 10 2016 09:08:28 with OCaml 4.01.0

$ ./configure ia32-linux
Testing assembler support for CFI directives... yes
Testing Coq... version 8.4pl2 -- good!

The below fails:

$ cat foo.c
struct X { int var; };

int main() {
        int num = sizeof(struct X);
        char* buf[num];
}
$ ccomp foo.c
foo.c:5: Error: array size is not a compile-time constant.
1 error detected.
$ gcc -std=c99 -pedantic foo.c
$

But this works:

$ cat foo.c
struct X { int var; };

int main() {
        char* buf[sizeof(struct X)];
}
$ ccomp foo.c
$

I would just like some information about the status of the memcpy built-in on the interpreter.

It seems that most of the code to enable its use is already present on Interp.ml/Cexec.v.

In theory, I might follow the example of printf in Interp.ml/do_external_function to add it, but I wonder if there are subtle issues which would prevent it from working properly, or if it has not been done simply by lack of demand/to minimize the amount of code to be maintained.

In the following code:

#include <stdio.h>

typedef struct __attribute((packed)) {
  int a:8;
  int b:9;
} st;

int main() {
  printf("sizeof(st) = %u\n", sizeof(st));
  return 0;
}

CompCert (configured with ia32-linux and run with -fbitfields -fpacked-structs) produces code which prints sizeof(st) = 4, while GCC and Clang both print sizeof(st) = 3.

Is it possible to tell CompCert to make it pack this structure using only 3 bytes? If not, is this due to a compiler-specific implementation choice, or related to ABI issues?

CompCert does not support "asm volatile" which is a common pattern I've seen:

$ cat foo.c
int
main(int argc, char **argv)
{
        __asm volatile("cli");
}
$ gcc foo.c
$ ccomp -finline-asm foo.c
foo.c:4: syntax error: expecting '}'.
foo.c:3: this is the location of the unclosed '{'.
Fatal error; compilation aborted.
1 error detected.

but "asm" is supported.

$ cat bar.c
int
main(int argc, char **argv)
{
        __asm ("cli");
}
$ gcc bar.c
$ ccomp -finline-asm bar.c
$

According to gcc documentation, gcc optimizers may eliminate asm statements. But using the volatile qualifier will disable any optimizations. (See https://gcc.gnu.org/onlinedocs/gcc/Extended-Asm.html#Volatile)

It would be useful if compcert would accept this syntax when using -finline-asm.

With CompCert 2.5, I've found that

wchar_t const abc[] = L"abc";

is somehow treated as

wchar_t const abc[] = { L'\0', L'a', L'b', L'c', L'\0' };

Meanwhile, wchar_t const *abc = L"abc" works as expected. I'm aware that wide character support is still a work in progress (#26), but this specific problem looks like it might point to some deeper issues.

I wanted to package CompCert, but I'd like to know before if the license prevent it or if there is any objections.

Latest Compcert fails to compile on OpenBSD. I'm using menhir version 20151103 and coq 8.4pl6. See below for the build error:

Linking ccomp
File "_none_", line 1:
Error: Files cparser/pre_parser.cmx
       and /usr/local/lib/ocaml/menhirLib/menhirLib.cmx
       make inconsistent assumptions over interface MenhirLib
Makefile.extr:81: recipe for target 'ccomp' failed

When trying to compile with -g I now get an error like the below which I think is new. (OpenBSD uses binutils 2.17 as this is the last GPLv2 version.)

$ cd /usr/src/bin/cat
$ ccomp -g cat.c
/tmp/compcert3db100.s: Assembler messages:
/tmp/compcert3db100.s:4: Error: unknown pseudo-op: `.cfi_sections'
Error during assembling.

The code in lines 52-59 of cparser/StructReturn.ml does not seem to correctly re-write function declarations of the form

struct a func(void);

The re-written output is:

extern void f(void);

When I guess it should be:

extern void f(struct a *);

Line 185 of the Makefile tries to remove doc/glob/$(*F).glob but it always fails because doc/glob/ does not exist. And indeed line 187 creates file doc/$(*F).glob, without the glob/ part.

Is this syntax error expected?

$ cat foo.c
struct x {
        int a;;
};

int main(int argc, char **argv) {
        struct x foo;

        foo.a = 1;
        return foo.a;
}
$ ccomp foo.c
foo.c:2: syntax error: expecting '}'.
foo.c:1: this is the location of the unclosed '{'.
Fatal error; compilation aborted.
1 error detected.

When "int a;;" is replace with "int a;" the above works as expected. Here's with gcc:

$ gcc -std=c99 -pedantic foo.c
foo.c:2: warning: extra semicolon in struct or union specified

With the current version, when I invoke ccomp -interp -fall a.c, it may generate many temporary files like
compcertb8d6b5.i in my temp folder. Those files remain there when ccomp quits.

The issue is gone when I revert to commit 54effdc.

I can't build CompCert 2.7.1 under cygwin on Windows 10.
The problem is that it requires menhir-2016xxxx.
This version of menhir doesn't build (although menhir-2015xxx did build),
because:

[from the Menhir "make"]:
Checking that OCaml is recent enough...
Cannot load required shared library dllcamlstr.
Reason: dllcamlstr.so: dynamic loading not supported on this platform.
File "checkOCamlVersion.ml", line 1:
Error: Reference to undefined global `Str'
Makefile:46: recipe for target '.versioncheck' failed

I have "The OCaml compiler, version 4.02.3".

I'm reporting this menhir problem to Francois Pottier.

Meanwhile, it's very annoying that every time I install a new
version of CompCert, I have to install a new menhir.
I BEG AND PLEAD WITH YOU: Distribute the OUTPUT of menhir
in the CompCert source distribution (and in the github repo).
That way, the 99% of us that do not need to change the C grammar,
will not need menhir.

$ menhir --version
menhir, version 20151112
$ cat test.c

int main(void) {
    return 100;
}

$ ./ccomp -dparse test.c
$ cat test.parsed.c

extern void __builtin_debug(int kind, ...);

int main(void)
{
  return 100;
  return 0;
}

I guess a bug was introduced with the recent changes in the lexer/parser as it does not happen with CompCert 2.5. The produced assembly code is not affected as the duplicate return is most likely removed during the optimizations (deadcode removal ?).

with gcc:

$ cat foo.c
#include <stdio.h>
void foo(void)
{
    puts("Hello Shared World");
}
$ gcc -fpic -std=c99 -c foo.c
$ gcc -shared -o libfoo.so foo.o
$

with CompCert this seems to work:

$ ccomp -fall -c foo.c
$ ccomp -Wl,-shared -o libfoo.so foo.c
$

But it would be nice to have support for -fpic.

The Makefile has an "install" target to put "ccomp" into a user-specified bin directory,
but there is no corresponding installer for clightgen.
[CompCert 2.6 distribution]

The code below produces unexpected results when compiled with CompCert.

$ cat foo.c
#include <stdio.h>
#include <stdlib.h>
#include <arpa/inet.h>

struct S {
    struct in_addr field;
};

int
main(int argc, char *argv[])
{
    struct S *s;

    s = calloc(1, sizeof(*s));
    printf("%s\n", inet_ntoa(s->field));
}
$ gcc foo.c
$ ./a.out
0.0.0.0
$ ccomp -fall foo.c
$ ./a.out
160.216.151.133

For the *.s files see here:
http://dickman.org/compcert/test23/

This works:

$ cat bar.c
int
main(int argc, char **argv)
{
    char hex[] = "0123456789ABCDEF";
}
$ ccomp bar.c
$

But this doesn't seem to:

$ cat foo.c
#include <wchar.h>

int
main(int argc, char **argv)
{
    wchar_t hex[] = L"0123456789ABCDEF";
}
$ ccomp foo.c
foo.c:6: Error:
  initialization of an array of non-wchar_t elements with a wide string literal.
foo.c:6: Warning: array of size 0.
1 error detected.

gcc compiles the above example without a problem.

$ gcc -std=c99 -pedantic foo.c
$

CompCert does not define a FLT_EVAL_METHOD macro, and due to the lack of long double, it normally would not fit into any of C99's 3 defined methods; but according to the user manual, would it be safe to assume CompCert's behavior as equivalent to FLT_EVAL_METHOD = 1 (intermediate expressions performed in double precision, as in K&R's C)? Or are there subtle differences which would prevent this?

I cannot get the offsetof macro to work …

#include <stddef.h>

struct toto {
  int x;
  int y;
};

int main()
{
  return offsetof(struct toto, y);
}

results in:

$ ccomp -c off2.c 
off2.c:10: syntax error: expecting ')'.
off2.c:10: this is the location of the unclosed '('.
Fatal error; compilation aborted.
1 error detected.

but the parentheses seem balanced in the preprocessor output:

$ ccomp -E off2.c | grep return
  return ((size_t) &(((struct toto)*) 0)->y);

In https://github.com/AbsInt/CompCert/blob/master/backend/RTL.v#L110, it mentions [fn_code_wf], and [fn_nextpc]. However, I cannot find [fn_code_wf]'s definition or usage. (I've greped whole repository)