CompCert for compiling C generated from ATS

[gmhwxi]

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!

[Yannick Duchêne]

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__=

[Hongwei Xi]

>> 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.

--
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.

[Yannick Duchêne]

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.

[Yannick Duchêne]

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.

[Hongwei Xi]

I made a small change to the Makefile.

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

make COMPCERT=ccomp

--
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.