CompCert for compiling C generated from ATS

Google Group
1

I felt that using CompCert to build ATS is a big thing that could be too
difficult to accomplish in one single step. Instead, let us focus on using
CompCert to compile C code generated from ATS source for the moment.

I created a compilation environment for this:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/CompCert

Basically, the header files in the following directory should replace those
default
one used by patscc:

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/CompCert/H

Please take a look at test00.dats and Makefile in

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/CompCert/TEST

If you do:

make test00; ./test00; echo $?

you should see ‘0’ being output. It is not much yet but it is a good start.

Cheers!

2

I made a small change to the Makefile.

If one does not want to create a symbolic link, then one can do

make COMPCERT=ccompOn Sun, Feb 1, 2015 at 3:36 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le dimanche 1 février 2015 21:32:13 UTC+1, Yannick Duchêne a écrit :

Le dimanche 1 février 2015 20:39:59 UTC+1, gmhwxi a écrit :

Why “export PATSCCOMP=gcc -std=c99” in the Makefile?

It is a placeholder for compcert. Now I have changed it:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/CompCert/TEST/Makefile

Oops, my bad, I troubled people minds in the other thread: the command
compcert is the one I use only me, using a symbolic link to ccomp,
which is the real command name. I created this symbolic link to avoid some
confusion with the same name appearing a many place in the source tree (I
grepped a lot while trying to compile ATS2). This is not an issue if the
Makefiles do the same, that’s OK, but then the creation of the link should
be advised somewhere. Or else, better use the real command name.

I will have a look at this Contrib later.

That said, looking at the Makefile, I really feel that’s better to create
a symbolic link, because the command’s real name is a lot confusing, as
it’s too generic. May be just adding something like “Please, ensure you
have a symbolic link to ccomp named compcert.” as a comment at the top of
Makefiles can be OK.

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/e63b0acc-c1f8-482c-b274-80c669027b48%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/e63b0acc-c1f8-482c-b274-80c669027b48%40googlegroups.com?utm_medium=email&utm_source=footer
.

3

Please take a look at test00.dats and Makefile in

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/CompCert/TEST

Why “export PATSCCOMP=gcc -std=c99” in the Makefile?

I rechecked the documentation, and here are the options which I feel should
be passed to CompCert to avoid some compilation issues:

  • -fbitfields
  • -flongdouble
  • -fpacked-structs
  • -fstruct-return

Also, as a reminder, here are options which may also be added when using
the GNU C library headers:

  • -D__GLIBC_HAVE_LONG_LONG=1
  • -D__signed__=
4

Why “export PATSCCOMP=gcc -std=c99” in the Makefile?

It is a placeholder for compcert. Now I have changed it:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/CompCert/TEST/Makefile

Oops, my bad, I troubled people minds in the other thread: the command
compcert is the one I use only me, using a symbolic link to ccomp,
which is the real command name. I created this symbolic link to avoid some
confusion with the same name appearing a many place in the source tree (I
grepped a lot while trying to compile ATS2). This is not an issue if the
Makefiles do the same, that’s OK, but then the creation of the link should
be advised somewhere. Or else, better use the real command name.

I will have a look at this Contrib later.

That said, looking at the Makefile, I really feel that’s better to create a
symbolic link, because the command’s real name is a lot confusing, as it’s
too generic. May be just adding something like “Please, ensure you have a
symbolic link to ccomp named compcert.” as a comment at the top of
Makefiles can be OK.

5

Why “export PATSCCOMP=gcc -std=c99” in the Makefile?

It is a placeholder for compcert. Now I have changed it:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/CompCert/TEST/Makefile

The next thing to do is to gradually modify the files in

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/CompCert/H

Right now, the compilation environment is the one for kernel programming,
which is too limited for
general purpose.On Sun, Feb 1, 2015 at 6:03 AM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Le dimanche 1 février 2015 06:10:57 UTC+1, gmhwxi a écrit :

Please take a look at test00.dats and Makefile in

https://github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/CompCert/TEST

Why “export PATSCCOMP=gcc -std=c99” in the Makefile?

I rechecked the documentation, and here are the options which I feel
should be passed to CompCert to avoid some compilation issues:

  • -fbitfields
  • -flongdouble
  • -fpacked-structs
  • -fstruct-return

Also, as a reminder, here are options which may also be added when using
the GNU C library headers:

  • -D__GLIBC_HAVE_LONG_LONG=1
  • -D__signed__=

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/a3a19d79-45cb-4cf5-8016-7a9714c2368e%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/a3a19d79-45cb-4cf5-8016-7a9714c2368e%40googlegroups.com?utm_medium=email&utm_source=footer
.

6

Why “export PATSCCOMP=gcc -std=c99” in the Makefile?

It is a placeholder for compcert. Now I have changed it:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/contrib/CompCert/TEST/Makefile

Oops, my bad, I troubled people minds in the other thread: the command
compcert is the one I use only me, using a symbolic link to ccomp,
which is the real command name. I created this symbolic link to avoid some
confusion with the same name appearing a many place in the source tree (I
grepped a lot while trying to compile ATS2). This is not an issue if the
Makefiles do the same, that’s OK, but then the creation of the link should
be advised somewhere. Or else, better use the real command name.

I will have a look at this Contrib later.