# Trying to build ATS2 with CompCert

**URL:** <https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119>\
**Category:** Google Group\
**Created:** [January 31, 2015, 10:15am UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119 "2015-01-31T10:15:19Z")\
**Posts on this page:** 16\
**Page:** 1

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [January 31, 2015, 10:15am UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/1 "2015-01-31T10:15:19Z")

</div>

After some quick and easy tweaks, I’m getting this, and as it’s in C files  
probably generated by ATS1, I feel to guess I can’t fix, and it suggest  
something would have to be tweaked in the C source generator.

```
 \
 make -j4 -C src/CBOOT \
 CCOMP=compcert GCFLAG=-D_ATS_NGC \
 CFLAGS= LDFLAGS= patsopt
 make[1]: entrant dans le répertoire « 

```

/home/yannick/Applications/Third\_Parties/ATS/ATS2-Postiats-0.1.8/src/CBOOT »  
compcert -I. -I./ccomp/runtime -c -o pats\_main\_dats.o pats\_main\_dats.c  
compcert -I. -I./ccomp/runtime -c -o pats\_utils\_sats.o  
pats\_utils\_sats.c  
compcert -I. -I./ccomp/runtime -c -o pats\_location\_sats.o  
pats\_location\_sats.c  
compcert -I. -I./ccomp/runtime -c -o pats\_jsonize\_sats.o  
pats\_jsonize\_sats.c  
./ccomp/runtime/ats\_types.h:68: Warning: empty struct.  
./ccomp/runtime/ats\_types.h:68: Warning: empty struct.  
./ccomp/runtime/ats\_types.h:68: Warning: empty struct.  
compcert -I. -I./ccomp/runtime -c -o pats\_errmsg\_sats.o  
pats\_errmsg\_sats.c  
./libc/sys/CATS/types.cats:72: Error: illegal comparison between types  
dev\_t  
and dev\_t.  
Fatal error; compilation aborted.  
1 error detected.  
make[1]: \*\*\* [pats\_utils\_sats.o] Erreur 2  
make[1]: \*\*\* Attente des tâches non terminées…  
./ccomp/runtime/ats\_types.h:68: Warning: empty struct.  
./ccomp/runtime/ats\_types.h:68: Warning: empty struct.  
prelude/CATS/bool.cats:45: Warning:  
redefinition of ‘ats\_exit\_errmsg’ with incompatible type.  
libc/sys/CATS/types.cats:72: Error: illegal comparison between types  
dev\_t  
and dev\_t.  
Fatal error; compilation aborted.  
1 error detected.  
make[1]: \*\*\* [pats\_main\_dats.o] Erreur 2  
make[1]: quittant le répertoire «  
/home/yannick/Applications/Third\_Parties/ATS/ATS2-Postiats-0.1.8/src/CBOOT »  
make: \*\*\* [src2\_patsopt] Erreur 2

Note the current directory for these messages, seems to be “src/CBOOT”.

The warning “./ccomp/runtime/ats\_types.h:68: Warning: empty struct.”, which  
appears five times, is about this:

```
 typedef struct{} ats_empty_type ;

```

OK, that’s just a warning.

The error “./libc/sys/CATS/types.cats:72: Error: illegal comparison between  
types dev\_t and dev\_t.”, which appears two times, is about this:

typedef dev\_t ats\_dev\_type ; // for device IDs

```
 ATSinline()
 ats_bool_type
 atslib_eq_dev_dev
   (dev_t x1, dev_t x2) {
   return (x1 == x2 ? ats_true_bool : ats_false_bool) ;
 } // end of [atslib_eq_dev_dev]

```

Line #72 is the one with “return (x1 == x2 ? ats\_true\_bool :  
ats\_false\_bool) ;”

I’m surprised with this one: is there a case where C99 disallow a  
comparison between two value of the same type? (here, `dev_t`).

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [January 31, 2015, 7:21pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/2 "2015-01-31T19:21:51Z")

</div>

> Hi Yannick,
> 
> This is all great!
> 
> It does seem quite plausible that we will be able to use compcert to  
> compile ATS in the  
> near future.
> 
> Could you also try to use compcert to compile some examples of C code  
> generated by ATS2?
> 
> For instance, the examples in the following directory are good ones:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/SHOOTOUT](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/SHOOTOUT)
> 
> These examples should give us a rough idea as to how compcert is compared  
> with gcc/clang in  
> terms of the efficiency of the generated object code.
> 
> Many thanks!

Just had a quick look building with GCC for a prior checkup. Some seems to  
require some data as input, but I don’t know where do I have to pick these  
data. Some work straight away, but are so fast I’m not sure I have to time  
them: are their execution time to be checked too? (must be a few  
milliseconds). Some others either crash or don’t compile, and I don’t know  
if it’s due to something wrong with my ATS2 (Postiat 0.1.8) or something  
else.

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [January 31, 2015, 1:16pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/3 "2015-01-31T13:16:16Z")

</div>

> Now it achieves compilation, but fails at link time, and I have so much  
> link errors I’m afraid. As a side note, during compilation, there is a lot  
> of warning messages.  
> The very long list of link error I get (enough for now, I may try to  
> resume later):

A last note: most of the link errors are about multiple definitions, and  
the warnings I get during compilation were about redefinitions with  
incompatible types. This seems related… What surprises me, is that there do  
not seems to be any issue with multiple definition at link time when ATS2  
is compiled with GCC.

Until now, for a summary, I would say compiling ATS2 would need three  
things and may be a fourth one:

- To know how to tell the GNU C includes files to not use ` __signed__ `
- To change configure so that it propagates de `CC` environment variable  
it recieves
- To use `memcmp` when nothing in POSIX and the C standard ensure a type  
is suitable for direct comparison (i.e. nothing ensure it’s a simple type)
- May be to not generate multiple definition, but that’s strange, as it’s  
not an issue when compiled with GCC.

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [January 31, 2015, 7:30pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/4 "2015-01-31T19:30:57Z")

</div>

These examples are taken from:

[http://benchmarksgame.alioth.debian.org/](http://benchmarksgame.alioth.debian.org/)

For now, let us focus on pidigits. On my machine, I got:

time ./pidigits 10000 \> /dev/null

real 0m1.006s  
user 0m0.996s  
sys 0m0.008s

time ./pidigits\_gcc 10000 \> /dev/null

real 0m1.004s  
user 0m1.000s  
sys 0m0.000s

What if we use compcert instead of gcc on pidigits and pidigits\_gcc?On Sat, Jan 31, 2015 at 2:21 PM, ‘Yannick Duchêne’ via ats-lang-users \< [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com)\> wrote:

> Le samedi 31 janvier 2015 19:36:46 UTC+1, gmhwxi a écrit :
> 
> > Hi Yannick,
> > 
> > This is all great!
> > 
> > It does seem quite plausible that we will be able to use compcert to  
> > compile ATS in the  
> > near future.
> > 
> > Could you also try to use compcert to compile some examples of C code  
> > generated by ATS2?
> > 
> > For instance, the examples in the following directory are good ones:
> > 
> > [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/SHOOTOUT](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/SHOOTOUT)
> > 
> > These examples should give us a rough idea as to how compcert is compared  
> > with gcc/clang in  
> > terms of the efficiency of the generated object code.
> > 
> > Many thanks!
> 
> Just had a quick look building with GCC for a prior checkup. Some seems to  
> require some data as input, but I don’t know where do I have to pick these  
> data. Some work straight away, but are so fast I’m not sure I have to time  
> them: are their execution time to be checked too? (must be a few  
> milliseconds). Some others either crash or don’t compile, and I don’t know  
> if it’s due to something wrong with my ATS2 (Postiat 0.1.8) or something  
> else.
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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/026704dc-895d-4a0f-843b-9c625f839ab4%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/026704dc-895d-4a0f-843b-9c625f839ab4%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/026704dc-895d-4a0f-843b-9c625f839ab4%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/026704dc-895d-4a0f-843b-9c625f839ab4%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [January 31, 2015, 8:05pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/5 "2015-01-31T20:05:54Z")

</div>

> > Some others either crash or don’t compile, and I don’t know if it’s due  
> > to something wrong with my ATS2 (Postiats 0.1.8) or something else.

I just tried. All the programs compiled on my machine. Let me know which  
ones did not compile on yours.

I also modified several Makefiles so that clang can also be used (except on  
those relying on gcc-eccentric features).On Sat, Jan 31, 2015 at 2:21 PM, ‘Yannick Duchêne’ via ats-lang-users \< [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com)\> wrote:

> Le samedi 31 janvier 2015 19:36:46 UTC+1, gmhwxi a écrit :
> 
> > Hi Yannick,
> > 
> > This is all great!
> > 
> > It does seem quite plausible that we will be able to use compcert to  
> > compile ATS in the  
> > near future.
> > 
> > Could you also try to use compcert to compile some examples of C code  
> > generated by ATS2?
> > 
> > For instance, the examples in the following directory are good ones:
> > 
> > [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/SHOOTOUT](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/SHOOTOUT)
> > 
> > These examples should give us a rough idea as to how compcert is compared  
> > with gcc/clang in  
> > terms of the efficiency of the generated object code.
> > 
> > Many thanks!
> 
> Just had a quick look building with GCC for a prior checkup. Some seems to  
> require some data as input, but I don’t know where do I have to pick these  
> data. Some work straight away, but are so fast I’m not sure I have to time  
> them: are their execution time to be checked too? (must be a few  
> milliseconds). Some others either crash or don’t compile, and I don’t know  
> if it’s due to something wrong with my ATS2 (Postiat 0.1.8) or something  
> else.
> 
> –  
> 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](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](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/026704dc-895d-4a0f-843b-9c625f839ab4%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/026704dc-895d-4a0f-843b-9c625f839ab4%40googlegroups.com)  
> [https://groups.google.com/d/msgid/ats-lang-users/026704dc-895d-4a0f-843b-9c625f839ab4%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/026704dc-895d-4a0f-843b-9c625f839ab4%40googlegroups.com?utm_medium=email&utm_source=footer)  
> .

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [January 31, 2015, 8:58pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/6 "2015-01-31T20:58:37Z")

</div>

> What about using `memcmp` for comparison of C types when these C types cannot be ensured to be simple type and so may possibly be compound types?

Any reason not to just use memcmp unconditionally? This is generated code after all.

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [January 31, 2015, 11:59am UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/7 "2015-01-31T11:59:05Z")

</div>

> Here is a short test:
> 
> ```
> #include <stdio.h>
> #include <sys/types.h>
> 
> typedef int ats_bool_type;
> #define ats_true_bool 1
> #define ats_false_bool 0
> 
> ats_bool_type atslib_eq_dev_dev (dev_t x1, dev_t x2) {
> return (x1 == x2 ? ats_true_bool : ats_false_bool) ;
> } // end of [atslib_eq_dev_dev]
> 
> int main (void) {
> printf("Hello!\n");
> printf("Size of `dev_t is` %i bytes\n", sizeof(dev_t));
> return 0;
> }
> 
> ```
> 
> Compilation fails with CompCert, even with this short snippet.
> 
> If I change the type of `x1` and `x2` to `int`, then it compiles, and says  
> the size of `dev_t` is 8 bytes.

May be a track.

First I tested two variations.

```
 typedef struct {
    int a;
    int b;
 } dev_t2;

 typedef long long dev_t3;

```

If the type of `x1` and `x2` is `dev_t2`, it fails with both GCC and  
CompCert, and if it is `dev_t3` it compiles with both GCC and CompCert.

I suspect a conditional definition which makes `dev_t` not be defiend the  
same when compiling with one or the other.

`dev_t` is defined as an alias of `__dev_t` which is defined to be  
` __DEV_T_TYPE` which is defined to be `__ UQUAD_TYPE`, which for machine  
with 32 bits words, is defined to be `__u_quad_t` and here, things may  
start to be wrong.

I have this:

```
 #if __WORDSIZE == 64
    typedef long int __quad_t;
    typedef unsigned long int __u_quad_t;
 #elif defined __GLIBC_HAVE_LONG_LONG
    __extension__ typedef long long int __quad_t;
    __extension__ typedef unsigned long long int __u_quad_t;
 #else
    typedef struct
    {
       long __val[2];
    } __quad_t;
    typedef struct
    {
       __u_long__ val[2];
    } __u_quad_t;
 #endif

```

I guessed when compiling with CompCert, `__GLIBC_HAVE_LONG_LONG` is false  
and it fall back to the `struct` definition, which does not allow  
comparison.

Indeed, compiling with `compcert -D__GLIBC_HAVE_LONG_LONG=1` make the build  
succeed.

However, that’s a trick, and may be there is a better way, but which  
involves modifying ATS1 which is used to generated C files for ATS2 (and  
ATS2 if in the future ATS2 is supposed to generate its own C files).

In [\<sys/types.h\>](http://pubs.opengroup.org/onlinepubs/009695399/basedefs/sys/types.h.html)  
nothing is asserted about `dev_t`. May when nothing assert a type is a  
simple type, comparison should be defined using `memcmp`. This should not  
be an issue, as a believe most C compiler will be able to optimize it when  
feasible.

What about using `memcmp` for comparison of C types when these C types  
cannot be ensured to be simple type and so may possibly be compound types?

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [January 31, 2015, 8:24pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/8 "2015-01-31T20:24:26Z")

</div>

> These examples are taken from:
> 
> [http://benchmarksgame.alioth.debian.org/](http://benchmarksgame.alioth.debian.org/)
> 
> For now, let us focus on pidigits. On my machine, I got:
> 
> time ./pidigits 10000 \> /dev/null
> 
> real 0m1.006s  
> user 0m0.996s  
> sys 0m0.008s
> 
> time ./pidigits\_gcc 10000 \> /dev/null
> 
> real 0m1.004s  
> user 0m1.000s  
> sys 0m0.000s
> 
> What if we use compcert instead of gcc on pidigits and pidigits\_gcc?

I’m stuck with a “syntax error” in `integer_fixed.cats` at line 58, the  
line “typedef int64\_t atstype\_int64 ;”

As CompCert seems to complain about syntax error when it encounters an  
undefined type, my guess is that it does not see the definition of the  
`atstype_int64`.

Here is the command I used:

```
 ccomp -v -I${PATSHOME} -I${PATSHOME}/ccomp/runtime 

```

-I/home/yannick/apps/ats/contrib pidigits\_dats.c

I can’t figure it out, but I will try again (just wanted to tell why I’m  
not posting the expected reply).

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [January 31, 2015, 11:12pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/9 "2015-01-31T23:12:32Z")

</div>

Yes, I should have used memcpy and let the compiler to optimize it  
away.

Will make changes shortly.On Saturday, January 31, 2015 at 3:58:39 PM UTC-5, Shea Levy wrote:

> > On Jan 31, 2015, at 11:59 AM, ‘Yannick Duchêne’ via ats-lang-users \< [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com) \<javascript:\>\> wrote:
> > 
> > What about using `memcmp` for comparison of C types when these C types  
> > cannot be ensured to be simple type and so may possibly be compound types?
> 
> Any reason not to just use memcmp unconditionally? This is generated code  
> after all.

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [January 31, 2015, 1:02pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/10 "2015-01-31T13:02:28Z")

</div>

> According to [The GNU C Reference Manual](http://www.gnu.org/software/gnu-c-manual/gnu-c-manual.html) ,  
> ` __signed__ ` is a GNU extension to C, so may be the headers must be told to  
> conform to C99, may be defining another macro on the command line, but I  
> don’t know which one. Some one who know GCC lib well have an idea?

Tried `-D_STDC_VERSION __=199901L` and `-D__ STDC__`, and this does not  
resolve the error. Tried `-D __signed__ =`, this solve the error, but I don’t  
like it, it looks like a hack, and there must be a proper configuration  
flag for this.

That said, although it looks like a trick, it proceed further and stop on  
errors about an unsupported feature with returning unions.Does not look to  
be a bad error, as CompCert suggest to just add the `-fstruct-return`  
option.

It proceed further again, and it stopped on another unsupported feature,  
with `long double`. For this one it does not suggest any option to add to  
the command line, but the documentation do. At “5.2.4.2 Numerical limits.”  
it says it required the option `-flongdouble`.

Now it achieves compilation, but fails at link time, and I have so much  
link errors I’m afraid. As a side note, during compilation, there is a lot  
of warning messages.

The very long list of link error I get (enough for now, I may try to resume  
later):

pats\_stamp\_dats.o: In function `aux_31_clofun': (.text+0x520): multiple definition of `aux\_31\_clofun’  
pats\_intinf\_dats.o:(.text+0x8b0): first defined here  
pats\_stamp\_dats.o: In function `aux_31_closure_make': (.text+0x560): multiple definition of `aux\_31\_closure\_make’  
pats\_intinf\_dats.o:(.text+0x8f0): first defined here  
pats\_parsing\_dats.o: In function `__ats_fun_3_clofun': (.text+0x150): multiple definition of `\_\_ats\_fun\_3\_clofun’  
pats\_reader\_dats.o:(.text+0xf0): first defined here  
pats\_parsing\_dats.o: In function `__ats_fun_3_closure_make': (.text+0x170): multiple definition of `\_\_ats\_fun\_3\_closure\_make’  
pats\_reader\_dats.o:(.text+0x110): first defined here  
pats\_trans1\_sort\_dats.o: In function `__ats_fun_5_clofun': (.text+0x190): multiple definition of `\_\_ats\_fun\_5\_clofun’  
pats\_reader\_dats.o:(.text+0x1b0): first defined here  
pats\_trans1\_sort\_dats.o: In function `__ats_fun_5_closure_make': (.text+0x1e0): multiple definition of `\_\_ats\_fun\_5\_closure\_make’  
pats\_reader\_dats.o:(.text+0x1c0): first defined here  
pats\_trans1\_sort\_dats.o: In function `__ats_fun_8_clofun': (.text+0x2c0): multiple definition of `\_\_ats\_fun\_8\_clofun’  
pats\_reader\_dats.o:(.text+0x300): first defined here  
pats\_trans1\_sort\_dats.o: In function `__ats_fun_8_closure_make': (.text+0x310): multiple definition of `\_\_ats\_fun\_8\_closure\_make’  
pats\_reader\_dats.o:(.text+0x320): first defined here  
pats\_trans1\_p0at\_dats.o: In function `appf_1_clofun': (.text+0x250): multiple definition of `appf\_1\_clofun’  
pats\_trans1\_sort\_dats.o:(.text+0x90): first defined here  
pats\_trans1\_p0at\_dats.o: In function `appf_1_closure_make': (.text+0x290): multiple definition of `appf\_1\_closure\_make’  
pats\_trans1\_sort\_dats.o:(.text+0xd0): first defined here  
pats\_trans1\_p0at\_dats.o: In function `__ats_fun_7_clofun': (.text+0x370): multiple definition of `\_\_ats\_fun\_7\_clofun’  
pats\_reader\_dats.o:(.text+0x270): first defined here  
pats\_trans1\_p0at\_dats.o: In function `__ats_fun_7_closure_make': (.text+0x3c0): multiple definition of `\_\_ats\_fun\_7\_closure\_make’  
pats\_reader\_dats.o:(.text+0x2a0): first defined here  
pats\_trans1\_p0at\_dats.o: In function `__ats_fun_10_clofun': (.text+0x4c0): multiple definition of `\_\_ats\_fun\_10\_clofun’  
pats\_reader\_dats.o:(.text+0x400): first defined here  
pats\_trans1\_p0at\_dats.o: In function `__ats_fun_10_closure_make': (.text+0x510): multiple definition of `\_\_ats\_fun\_10\_closure\_make’  
pats\_reader\_dats.o:(.text+0x420): first defined here  
pats\_trans1\_p0at\_dats.o: In function `f_16_clofun': (.text+0x700): multiple definition of `f\_16\_clofun’  
pats\_fixity\_fxty\_dats.o:(.text+0xaa0): first defined here  
pats\_trans1\_p0at\_dats.o: In function `f_16_closure_make': (.text+0x740): multiple definition of `f\_16\_closure\_make’  
pats\_fixity\_fxty\_dats.o:(.text+0xaf0): first defined here  
pats\_trans1\_syndef\_dats.o: In function `__ats_fun_12_clofun': (.text+0x360): multiple definition of `\_\_ats\_fun\_12\_clofun’  
pats\_trans1\_e0xp\_dats.o:(.text+0x880): first defined here  
pats\_trans1\_syndef\_dats.o: In function `__ats_fun_12_closure_make': (.text+0x3a0): multiple definition of `\_\_ats\_fun\_12\_closure\_make’  
pats\_trans1\_e0xp\_dats.o:(.text+0x8d0): first defined here  
pats\_trans1\_dynexp\_dats.o: In function `__ats_fun_8_clofun': (.text+0x3e0): multiple definition of `\_\_ats\_fun\_8\_clofun’  
pats\_reader\_dats.o:(.text+0x300): first defined here  
pats\_trans1\_dynexp\_dats.o: In function `__ats_fun_8_closure_make': (.text+0x430): multiple definition of `\_\_ats\_fun\_8\_closure\_make’  
pats\_reader\_dats.o:(.text+0x320): first defined here  
pats\_trans1\_dynexp\_dats.o: In function `__ats_fun_11_clofun': (.text+0x530): multiple definition of `\_\_ats\_fun\_11\_clofun’  
pats\_reader\_dats.o:(.text+0x4e0): first defined here  
pats\_trans1\_dynexp\_dats.o: In function `__ats_fun_11_closure_make': (.text+0x580): multiple definition of `\_\_ats\_fun\_11\_closure\_make’  
pats\_reader\_dats.o:(.text+0x500): first defined here  
pats\_staexp2\_pprint\_dats.o: In function `loop_9_clofun': (.text+0x1b50): multiple definition of `loop\_9\_clofun’  
pats\_symbol\_dats.o:(.text+0x180): first defined here  
pats\_staexp2\_pprint\_dats.o: In function `loop_9_closure_make': (.text+0x1ba0): multiple definition of `loop\_9\_closure\_make’  
pats\_symbol\_dats.o:(.text+0x1e0): first defined here  
pats\_staexp2\_pprint\_dats.o: In function `loop_10_clofun': (.text+0x1cd0): multiple definition of `loop\_10\_clofun’  
pats\_lexing\_token\_dats.o:(.text+0x1c0): first defined here  
pats\_staexp2\_pprint\_dats.o: In function `loop_10_closure_make': (.text+0x1d20): multiple definition of `loop\_10\_closure\_make’  
pats\_lexing\_token\_dats.o:(.text+0x220): first defined here  
pats\_staexp2\_pprint\_dats.o: In function `loop_11_clofun': (.text+0x1eb0): multiple definition of `loop\_11\_clofun’  
pats\_lexing\_dats.o:(.text+0x230): first defined here  
pats\_staexp2\_pprint\_dats.o: In function `loop_11_closure_make': (.text+0x1f00): multiple definition of `loop\_11\_closure\_make’  
pats\_lexing\_dats.o:(.text+0x290): first defined here  
pats\_staexp2\_svar\_dats.o: In function `aux_26_clofun': (.text+0x670): multiple definition of `aux\_26\_clofun’  
pats\_staexp2\_pprint\_dats.o:(.text+0x2af0): first defined here  
pats\_staexp2\_svar\_dats.o: In function `aux_26_closure_make': (.text+0x6c0): multiple definition of `aux\_26\_closure\_make’  
pats\_staexp2\_pprint\_dats.o:(.text+0x2b40): first defined here  
pats\_staexp2\_svvar\_dats.o: In function `insert_34_clofun': (.text+0xb10): multiple definition of `insert\_34\_clofun’  
pats\_staexp2\_svar\_dats.o:(.text+0xe00): first defined here  
pats\_staexp2\_svvar\_dats.o: In function `insert_34_closure_make': (.text+0xb60): multiple definition of `insert\_34\_closure\_make’  
pats\_staexp2\_svar\_dats.o:(.text+0xe50): first defined here  
pats\_staexp2\_skexp\_dats.o: In function `aux_2_clofun': (.text+0xa0): multiple definition of `aux\_2\_clofun’  
pats\_dynexp1\_print\_dats.o:(.text+0x100): first defined here  
pats\_staexp2\_skexp\_dats.o: In function `aux_2_closure_make': (.text+0xf0): multiple definition of `aux\_2\_closure\_make’  
pats\_dynexp1\_print\_dats.o:(.text+0x150): first defined here  
pats\_patcst2\_dats.o: In function `aux_64_clofun': (.text+0x2280): multiple definition of `aux\_64\_clofun’  
pats\_staexp2\_svvar\_dats.o:(.text+0x1740): first defined here  
pats\_patcst2\_dats.o: In function `aux_64_closure_make': (.text+0x22b0): multiple definition of `aux\_64\_closure\_make’  
pats\_staexp2\_svvar\_dats.o:(.text+0x1790): first defined here  
pats\_dynexp2\_print\_dats.o: In function `aux_5_clofun': (.text+0x4f0): multiple definition of `aux\_5\_clofun’  
pats\_staexp1\_print\_dats.o:(.text+0x3f0): first defined here  
pats\_dynexp2\_print\_dats.o: In function `aux_5_closure_make': (.text+0x540): multiple definition of `aux\_5\_closure\_make’  
pats\_staexp1\_print\_dats.o:(.text+0x440): first defined here  
pats\_dynexp2\_dcst\_dats.o: In function `__ats_fun_37_clofun': (.text+0x750): multiple definition of `\_\_ats\_fun\_37\_clofun’  
pats\_patcst2\_dats.o:(.text+0x1030): first defined here  
pats\_dynexp2\_dcst\_dats.o: In function `aux_42_clofun': (.text+0x890): multiple definition of `aux\_42\_clofun’  
pats\_intinf\_dats.o:(.text+0xd40): first defined here  
pats\_dynexp2\_dcst\_dats.o: In function `aux_42_closure_make': (.text+0x8d0): multiple definition of `aux\_42\_closure\_make’  
pats\_intinf\_dats.o:(.text+0xd90): first defined here  
pats\_dynexp2\_dvar\_dats.o: In function `__ats_fun_50_clofun': (.text+0xde0): multiple definition of `\_\_ats\_fun\_50\_clofun’  
pats\_patcst2\_dats.o:(.text+0x17c0): first defined here  
pats\_dynexp2\_dvar\_dats.o: In function `__ats_fun_50_closure_make': (.text+0xe20): multiple definition of `\_\_ats\_fun\_50\_closure\_make’  
pats\_patcst2\_dats.o:(.text+0x17f0): first defined here  
pats\_dynexp2\_dvar\_dats.o: In function `insert_99_clofun': (.text+0x2950): multiple definition of `insert\_99\_clofun’  
pats\_staexp2\_scst\_dats.o:(.text+0x2630): first defined here  
pats\_dynexp2\_dvar\_dats.o: In function `insert_99_closure_make': (.text+0x29a0): multiple definition of `insert\_99\_closure\_make’  
pats\_staexp2\_scst\_dats.o:(.text+0x2680): first defined here  
pats\_trans2\_env\_dats.o: In function `f_12_clofun': (.text+0x1d0): multiple definition of `f\_12\_clofun’  
pats\_fixity\_fxty\_dats.o:(.text+0x580): first defined here  
pats\_trans2\_env\_dats.o: In function `f_12_closure_make': (.text+0x200): multiple definition of `f\_12\_closure\_make’  
pats\_fixity\_fxty\_dats.o:(.text+0x5d0): first defined here  
pats\_trans2\_env\_dats.o: In function `f_27_clofun': (.text+0x6d0): multiple definition of `f\_27\_clofun’  
pats\_trans1\_staexp\_dats.o:(.text+0x980): first defined here  
pats\_trans2\_env\_dats.o: In function `f_27_closure_make': (.text+0x700): multiple definition of `f\_27\_closure\_make’  
pats\_trans1\_staexp\_dats.o:(.text+0x9b0): first defined here  
pats\_trans2\_staexp\_dats.o: In function `aux_62_clofun': (.text+0x2eb0): multiple definition of `aux\_62\_clofun’  
pats\_trans2\_env\_dats.o:(.text+0x1390): first defined here  
pats\_trans2\_staexp\_dats.o: In function `aux_62_closure_make': (.text+0x2ef0): multiple definition of `aux\_62\_closure\_make’  
pats\_trans2\_env\_dats.o:(.text+0x13d0): first defined here  
pats\_trans2\_dynexp\_dats.o: In function `__ats_fun_15_clofun': (.text+0xd10): multiple definition of `\_\_ats\_fun\_15\_clofun’  
pats\_trans1\_syndef\_dats.o:(.text+0x4e0): first defined here  
pats\_trans2\_impdec\_dats.o: In function `auxerr1_24_clofun': (.text+0x16c0): multiple definition of `auxerr1\_24\_clofun’  
pats\_trans2\_staexp\_dats.o:(.text+0x1010): first defined here  
pats\_trans2\_impdec\_dats.o: In function `auxerr1_24_closure_make': (.text+0x16e0): multiple definition of `auxerr1\_24\_closure\_make’  
pats\_trans2\_staexp\_dats.o:(.text+0x1060): first defined here  
pats\_trans2\_impdec\_dats.o: In function `auxerr2_25_clofun': (.text+0x1870): multiple definition of `auxerr2\_25\_clofun’  
pats\_trans2\_staexp\_dats.o:(.text+0x11f0): first defined here  
pats\_trans2\_impdec\_dats.o: In function `auxerr2_25_closure_make': (.text+0x18b0): multiple definition of `auxerr2\_25\_closure\_make’  
pats\_trans2\_staexp\_dats.o:(.text+0x1240): first defined here  
pats\_dynexp3\_print\_dats.o: In function `aux_5_clofun': (.text+0xa20): multiple definition of `aux\_5\_clofun’  
pats\_staexp1\_print\_dats.o:(.text+0x3f0): first defined here  
pats\_dynexp3\_print\_dats.o: In function `aux_5_closure_make': (.text+0xa70): multiple definition of `aux\_5\_closure\_make’  
pats\_staexp1\_print\_dats.o:(.text+0x440): first defined here  
pats\_trans3\_env\_lstate\_dats.o: In function `aux_5_clofun': (.text+0x2d0): multiple definition of `aux\_5\_clofun’  
pats\_staexp1\_print\_dats.o:(.text+0x3f0): first defined here  
pats\_trans3\_env\_lstate\_dats.o: In function `aux_5_closure_make': (.text+0x320): multiple definition of `aux\_5\_closure\_make’  
pats\_staexp1\_print\_dats.o:(.text+0x440): first defined here  
pats\_dmacro2\_print\_dats.o: In function `aux_2_clofun': (.text+0xa0): multiple definition of `aux\_2\_clofun’  
pats\_dynexp1\_print\_dats.o:(.text+0x100): first defined here  
pats\_dmacro2\_print\_dats.o: In function `aux_2_closure_make': (.text+0xf0): multiple definition of `aux\_2\_closure\_make’  
pats\_dynexp1\_print\_dats.o:(.text+0x150): first defined here  
pats\_trans3\_p2at\_dats.o: In function `aux_21_clofun': (.text+0xbb0): multiple definition of `aux\_21\_clofun’  
pats\_utils\_dats.o:(.text+0x900): first defined here  
pats\_trans3\_p2at\_dats.o: In function `aux_21_closure_make': (.text+0xc10): multiple definition of `aux\_21\_closure\_make’  
pats\_utils\_dats.o:(.text+0x940): first defined here  
pats\_trans3\_dynexp\_dn\_dats.o: In function `__ats_fun_7_clofun': (.text+0x3d0): multiple definition of `\_\_ats\_fun\_7\_clofun’  
pats\_reader\_dats.o:(.text+0x270): first defined here  
pats\_trans3\_caseof\_dats.o: In function `auxerr_15_clofun': (.text+0x9b0): multiple definition of `auxerr\_15\_clofun’  
pats\_trans3\_env\_effect\_dats.o:(.text+0x590): first defined here  
pats\_trans3\_caseof\_dats.o: In function `auxerr_15_closure_make': (.text+0x9f0): multiple definition of `auxerr\_15\_closure\_make’  
pats\_trans3\_env\_effect\_dats.o:(.text+0x5d0): first defined here  
pats\_trans3\_caseof\_dats.o: In function `aux_21_clofun': (.text+0xdf0): multiple definition of `aux\_21\_clofun’  
pats\_utils\_dats.o:(.text+0x900): first defined here  
pats\_trans3\_caseof\_dats.o: In function `aux_21_closure_make': (.text+0xe20): multiple definition of `aux\_21\_closure\_make’  
pats\_utils\_dats.o:(.text+0x940): first defined here  
pats\_trans3\_decl\_dats.o: In function `aux_10_clofun': (.text+0x740): multiple definition of `aux\_10\_clofun’  
pats\_trans3\_env\_print\_dats.o:(.text+0xc00): first defined here  
pats\_trans3\_decl\_dats.o: In function `aux_10_closure_make': (.text+0x770): multiple definition of `aux\_10\_closure\_make’  
pats\_trans3\_env\_print\_dats.o:(.text+0xc50): first defined here  
pats\_constraint3\_print\_dats.o: In function `aux_5_clofun': (.text+0xe60): multiple definition of `aux\_5\_clofun’  
pats\_staexp1\_print\_dats.o:(.text+0x3f0): first defined here  
pats\_constraint3\_print\_dats.o: In function `aux_5_closure_make': (.text+0xeb0): multiple definition of `aux\_5\_closure\_make’  
pats\_staexp1\_print\_dats.o:(.text+0x440): first defined here  
pats\_constraint3\_simplify\_dats.o: In function `__ats_fun_22_clofun': (.text+0xa10): multiple definition of `\_\_ats\_fun\_22\_clofun’  
pats\_stamp\_dats.o:(.text+0x360): first defined here  
pats\_constraint3\_simplify\_dats.o: In function `__ats_fun_22_closure_make': (.text+0xa40): multiple definition of `\_\_ats\_fun\_22\_closure\_make’  
pats\_stamp\_dats.o:(.text+0x3a0): first defined here  
pats\_histaexp\_print\_dats.o: In function `aux_2_clofun': (.text+0xa0): multiple definition of `aux\_2\_clofun’  
pats\_dynexp1\_print\_dats.o:(.text+0x100): first defined here  
pats\_histaexp\_print\_dats.o: In function `aux_2_closure_make': (.text+0xf0): multiple definition of `aux\_2\_closure\_make’  
pats\_dynexp1\_print\_dats.o:(.text+0x150): first defined here  
pats\_hidynexp\_print\_dats.o: In function `aux_5_clofun': (.text+0xaa0): multiple definition of `aux\_5\_clofun’  
pats\_staexp1\_print\_dats.o:(.text+0x3f0): first defined here  
pats\_hidynexp\_print\_dats.o: In function `aux_5_closure_make': (.text+0xaf0): multiple definition of `aux\_5\_closure\_make’  
pats\_staexp1\_print\_dats.o:(.text+0x440): first defined here  
pats\_typerase\_decl\_dats.o: In function `__ats_fun_22_clofun': (.text+0x9d0): multiple definition of `\_\_ats\_fun\_22\_clofun’  
pats\_stamp\_dats.o:(.text+0x360): first defined here  
pats\_typerase\_decl\_dats.o: In function `__ats_fun_22_closure_make': (.text+0xa00): multiple definition of `\_\_ats\_fun\_22\_closure\_make’  
pats\_stamp\_dats.o:(.text+0x3a0): first defined here  
pats\_ccomp\_print\_dats.o: In function `aux_3_clofun': (.text+0x2a0): multiple definition of `aux\_3\_clofun’  
pats\_staexp2\_szexp\_dats.o:(.text+0xa0): first defined here  
pats\_ccomp\_print\_dats.o: In function `aux_3_closure_make': (.text+0x2f0): multiple definition of `aux\_3\_closure\_make’  
pats\_staexp2\_szexp\_dats.o:(.text+0xf0): first defined here  
pats\_ccomp\_print\_dats.o: In function `aux_25_clofun': (.text+0x35b0): multiple definition of `aux\_25\_clofun’  
pats\_utils\_dats.o:(.text+0xc20): first defined here  
pats\_ccomp\_print\_dats.o: In function `aux_25_closure_make': (.text+0x3600): multiple definition of `aux\_25\_closure\_make’  
pats\_utils\_dats.o:(.text+0xc70): first defined here  
pats\_ccomp\_hitype\_dats.o: In function `aux_3_clofun': (.text+0x820): multiple definition of `aux\_3\_clofun’  
pats\_staexp2\_szexp\_dats.o:(.text+0xa0): first defined here  
pats\_ccomp\_hitype\_dats.o: In function `aux_3_closure_make': (.text+0x870): multiple definition of `aux\_3\_closure\_make’  
pats\_staexp2\_szexp\_dats.o:(.text+0xf0): first defined here  
pats\_ccomp\_tmpvar\_dats.o: In function `__ats_fun_21_clofun': (.text+0x5c0): multiple definition of `\_\_ats\_fun\_21\_clofun’  
pats\_symmap\_dats.o:(.text+0xae0): first defined here  
pats\_ccomp\_tmpvar\_dats.o: In function `insert_53_clofun': (.text+0x1590): multiple definition of `insert\_53\_clofun’  
pats\_dynexp2\_dcst\_dats.o:(.text+0x1440): first defined here  
pats\_ccomp\_tmpvar\_dats.o: In function `insert_53_closure_make': (.text+0x15e0): multiple definition of `insert\_53\_closure\_make’  
pats\_dynexp2\_dcst\_dats.o:(.text+0x1480): first defined here  
pats\_ccomp\_d2env\_dats.o: In function `__ats_fun_4_clofun': (.text+0x120): multiple definition of `\_\_ats\_fun\_4\_clofun’  
pats\_dynexp2\_util\_dats.o:(.text+0x140): first defined here  
pats\_ccomp\_d2env\_dats.o: In function `insert_12_clofun': (.text+0x6c0): multiple definition of `insert\_12\_clofun’  
pats\_symmap\_dats.o:(.text+0x780): first defined here  
pats\_ccomp\_d2env\_dats.o: In function `insert_12_closure_make': (.text+0x700): multiple definition of `insert\_12\_closure\_make’  
pats\_symmap\_dats.o:(.text+0x7d0): first defined here  
pats\_ccomp\_funent\_dats.o: In function `aux_19_clofun': (.text+0x420): multiple definition of `aux\_19\_clofun’  
pats\_patcst2\_dats.o:(.text+0xac0): first defined here  
pats\_ccomp\_funent\_dats.o: In function `aux_19_closure_make': (.text+0x470): multiple definition of `aux\_19\_closure\_make’  
pats\_patcst2\_dats.o:(.text+0xb10): first defined here  
pats\_ccomp\_claulst\_dats.o: In function `aux_12_clofun': (.text+0xbb0): multiple definition of `aux\_12\_clofun’  
pats\_dynexp2\_dmac\_dats.o:(.text+0x330): first defined here  
pats\_ccomp\_claulst\_dats.o: In function `aux_12_closure_make': (.text+0xc00): multiple definition of `aux\_12\_closure\_make’  
pats\_dynexp2\_dmac\_dats.o:(.text+0x380): first defined here  
prelude\_libats.o: In function `__ats_fun_29_clofun': (.text+0x2300): multiple definition of `\_\_ats\_fun\_29\_clofun’  
pats\_staexp2\_svar\_dats.o:(.text+0x850): first defined here  
prelude\_libats.o: In function `__ats_fun_22_clofun': (.text+0x1f90): multiple definition of `\_\_ats\_fun\_22\_clofun’  
pats\_stamp\_dats.o:(.text+0x360): first defined here  
prelude\_libats.o: In function `__ats_fun_5_clofun': (.text+0x2f90): multiple definition of `\_\_ats\_fun\_5\_clofun’  
pats\_reader\_dats.o:(.text+0x1b0): first defined here  
prelude\_libats.o: In function `__ats_fun_29_closure_make': (.text+0x2320): multiple definition of `\_\_ats\_fun\_29\_closure\_make’  
pats\_staexp2\_svar\_dats.o:(.text+0x890): first defined here  
prelude\_libats.o: In function `__ats_fun_22_closure_make': (.text+0x1fb0): multiple definition of `\_\_ats\_fun\_22\_closure\_make’  
pats\_stamp\_dats.o:(.text+0x3a0): first defined here  
pats\_main\_dats.o: In function  
`_2home_2hwxi_2research_2Postiats_2git_2src_2pats_main_2edats__do_transfinal2': (.text+0x1928): undefined reference to `alloca’  
pats\_staexp2\_skexp\_dats.o: In function  
`_2home_2hwxi_2research_2Postiats_2git_2src_2pats_staexp2_util_2esats__s2kexp_ismat': (.text+0x1421): undefined reference to `alloca’  
pats\_staexp2\_skexp\_dats.o: In function  
`_2home_2hwxi_2research_2Postiats_2git_2src_2pats_staexp2_util_2esats__s2kexplst_ismat': (.text+0x14e1): undefined reference to `alloca’  
pats\_staexp2\_szexp\_dats.o: In function  
`_2home_2hwxi_2research_2Postiats_2git_2src_2pats_staexp2_util_2esats__s2zexp_merge': (.text+0x18a1): undefined reference to `alloca’  
pats\_staexp2\_util2\_dats.o: In function  
`_2home_2hwxi_2research_2Postiats_2git_2src_2pats_staexp2_util_2esats__s2hnf_syneq': (.text+0xb91): undefined reference to `alloca’  
pats\_staexp2\_util2\_dats.o:(.text+0xc51): more undefined references to  
`alloca’ follow  
collect2: ld a retourné 1 code d’état d’exécution

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [January 31, 2015, 11:34pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/11 "2015-01-31T23:34:08Z")

</div>

Okay, I have got eq\_dev\_dev (and eq\_ino\_ino) fixed.On Saturday, January 31, 2015 at 6:59:05 AM UTC-5, Yannick Duchêne wrote:

> Le samedi 31 janvier 2015 12:07:48 UTC+1, Yannick Duchêne a écrit :
> 
> > Here is a short test:
> > 
> > ```
> > #include <stdio.h>
> > #include <sys/types.h>
> > 
> > typedef int ats_bool_type;
> > #define ats_true_bool 1
> > #define ats_false_bool 0
> > 
> > ats_bool_type atslib_eq_dev_dev (dev_t x1, dev_t x2) {
> > return (x1 == x2 ? ats_true_bool : ats_false_bool) ;
> > } // end of [atslib_eq_dev_dev]
> > 
> > int main (void) {
> > printf("Hello!\n");
> > printf("Size of `dev_t is` %i bytes\n", sizeof(dev_t));
> > return 0;
> > }
> > 
> > ```
> > 
> > Compilation fails with CompCert, even with this short snippet.
> > 
> > If I change the type of `x1` and `x2` to `int`, then it compiles, and  
> > says the size of `dev_t` is 8 bytes.
> 
> May be a track.
> 
> First I tested two variations.
> 
> ```
> typedef struct {
> int a;
> int b;
> } dev_t2;
> 
> typedef long long dev_t3;
> 
> ```
> 
> If the type of `x1` and `x2` is `dev_t2`, it fails with both GCC and  
> CompCert, and if it is `dev_t3` it compiles with both GCC and CompCert.
> 
> I suspect a conditional definition which makes `dev_t` not be defiend the  
> same when compiling with one or the other.
> 
> `dev_t` is defined as an alias of `__dev_t` which is defined to be  
> ` __DEV_T_TYPE` which is defined to be `__ UQUAD_TYPE`, which for machine  
> with 32 bits words, is defined to be `__u_quad_t` and here, things may  
> start to be wrong.
> 
> I have this:
> 
> ```
> #if __WORDSIZE == 64
> typedef long int __quad_t;
> typedef unsigned long int __u_quad_t;
> #elif defined __GLIBC_HAVE_LONG_LONG
> __extension__ typedef long long int __quad_t;
> __extension__ typedef unsigned long long int __u_quad_t;
> #else
> typedef struct
> {
> long __val[2];
> } __quad_t;
> typedef struct
> {
> __u_long__ val[2];
> } __u_quad_t;
> #endif
> 
> ```
> 
> I guessed when compiling with CompCert, `__GLIBC_HAVE_LONG_LONG` is false  
> and it fall back to the `struct` definition, which does not allow  
> comparison.
> 
> Indeed, compiling with `compcert -D__GLIBC_HAVE_LONG_LONG=1` make the  
> build succeed.
> 
> However, that’s a trick, and may be there is a better way, but which  
> involves modifying ATS1 which is used to generated C files for ATS2 (and  
> ATS2 if in the future ATS2 is supposed to generate its own C files).
> 
> In  
> [\<sys/types.h\>](http://pubs.opengroup.org/onlinepubs/009695399/basedefs/sys/types.h.html)  
> nothing is asserted about `dev_t`. May when nothing assert a type is a  
> simple type, comparison should be defined using `memcmp`. This should not  
> be an issue, as a believe most C compiler will be able to optimize it when  
> feasible.
> 
> What about using `memcmp` for comparison of C types when these C types  
> cannot be ensured to be simple type and so may possibly be compound types?

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [January 31, 2015, 11:07am UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/12 "2015-01-31T11:07:48Z")

</div>

> The error “./libc/sys/CATS/types.cats:72: Error: illegal comparison  
> between types dev\_t and dev\_t.”, which appears two times, is about this:
> 
> typedef dev\_t ats\_dev\_type ; // for device IDs
> 
> ```
> ATSinline()
> ats_bool_type
> atslib_eq_dev_dev
> (dev_t x1, dev_t x2) {
> return (x1 == x2 ? ats_true_bool : ats_false_bool) ;
> } // end of [atslib_eq_dev_dev]
> 
> ```
> 
> Line #72 is the one with “return (x1 == x2 ? ats\_true\_bool :  
> ats\_false\_bool) ;”
> 
> I’m surprised with this one: is there a case where C99 disallow a  
> comparison between two value of the same type? (here, `dev_t`).

Here is a short test:

```
 #include <stdio.h>
 #include <sys/types.h>

 typedef int ats_bool_type;
 #define ats_true_bool 1
 #define ats_false_bool 0

 ats_bool_type atslib_eq_dev_dev (dev_t x1, dev_t x2) {
    return (x1 == x2 ? ats_true_bool : ats_false_bool) ;
 } // end of [atslib_eq_dev_dev]

 int main (void) {
    printf("Hello!\n");
    printf("Size of `dev_t is` %i bytes\n", sizeof(dev_t));
    return 0;
 }

```

Compilation fails with CompCert, even with this short snippet.

If I change the type of `x1` and `x2` to `int`, then it compiles, and says  
the size of `dev_t` is 8 bytes.

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [January 31, 2015, 12:01pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/13 "2015-01-31T12:01:40Z")

</div>

> Indeed, compiling with `compcert -D__GLIBC_HAVE_LONG_LONG=1` make the  
> build succeed.

To clarify it, I meant the build of the tiny test file, not the build of  
ATS2 (I will test it later).

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [January 31, 2015, 6:36pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/14 "2015-01-31T18:36:46Z")

</div>

Hi Yannick,

This is all great!

It does seem quite plausible that we will be able to use compcert to  
compile ATS in the  
near future.

Could you also try to use compcert to compile some examples of C code  
generated by ATS2?

For instance, the examples in the following directory are good ones:

> <https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/SHOOTOUT>
>
> //github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/SHOOTOUT

These examples should give us a rough idea as to how compcert is compared  
with gcc/clang in  
terms of the efficiency of the generated object code.

Many thanks!On Saturday, January 31, 2015 at 5:15:20 AM UTC-5, Yannick Duchêne wrote:

> After some quick and easy tweaks, I’m getting this, and as it’s in C files  
> probably generated by ATS1, I feel to guess I can’t fix, and it suggest  
> something would have to be tweaked in the C source generator.
> 
> ```
> \
> make -j4 -C src/CBOOT \
> CCOMP=compcert GCFLAG=-D_ATS_NGC \
> CFLAGS= LDFLAGS= patsopt
> make[1]: entrant dans le répertoire « 
> 
> ```
> 
> /home/yannick/Applications/Third\_Parties/ATS/ATS2-Postiats-0.1.8/src/CBOOT »  
> compcert -I. -I./ccomp/runtime -c -o pats\_main\_dats.o pats\_main\_dats.c  
> compcert -I. -I./ccomp/runtime -c -o pats\_utils\_sats.o  
> pats\_utils\_sats.c  
> compcert -I. -I./ccomp/runtime -c -o pats\_location\_sats.o  
> pats\_location\_sats.c  
> compcert -I. -I./ccomp/runtime -c -o pats\_jsonize\_sats.o  
> pats\_jsonize\_sats.c  
> ./ccomp/runtime/ats\_types.h:68: Warning: empty struct.  
> ./ccomp/runtime/ats\_types.h:68: Warning: empty struct.  
> ./ccomp/runtime/ats\_types.h:68: Warning: empty struct.  
> compcert -I. -I./ccomp/runtime -c -o pats\_errmsg\_sats.o  
> pats\_errmsg\_sats.c  
> ./libc/sys/CATS/types.cats:72: Error: illegal comparison between  
> types dev\_t  
> and dev\_t.  
> Fatal error; compilation aborted.  
> 1 error detected.  
> make[1]: \*\*\* [pats\_utils\_sats.o] Erreur 2  
> make[1]: \*\*\* Attente des tâches non terminées…  
> ./ccomp/runtime/ats\_types.h:68: Warning: empty struct.  
> ./ccomp/runtime/ats\_types.h:68: Warning: empty struct.  
> prelude/CATS/bool.cats:45: Warning:  
> redefinition of ‘ats\_exit\_errmsg’ with incompatible type.  
> libc/sys/CATS/types.cats:72: Error: illegal comparison between types  
> dev\_t  
> and dev\_t.  
> Fatal error; compilation aborted.  
> 1 error detected.  
> make[1]: \*\*\* [pats\_main\_dats.o] Erreur 2  
> make[1]: quittant le répertoire «  
> /home/yannick/Applications/Third\_Parties/ATS/ATS2-Postiats-0.1.8/src/CBOOT »  
> make: \*\*\* [src2\_patsopt] Erreur 2
> 
> Note the current directory for these messages, seems to be “src/CBOOT”.
> 
> The warning “./ccomp/runtime/ats\_types.h:68: Warning: empty struct.”,  
> which appears five times, is about this:
> 
> ```
> typedef struct{} ats_empty_type ;
> 
> ```
> 
> OK, that’s just a warning.
> 
> The error “./libc/sys/CATS/types.cats:72: Error: illegal comparison  
> between types dev\_t and dev\_t.”, which appears two times, is about this:
> 
> typedef dev\_t ats\_dev\_type ; // for device IDs
> 
> ```
> ATSinline()
> ats_bool_type
> atslib_eq_dev_dev
> (dev_t x1, dev_t x2) {
> return (x1 == x2 ? ats_true_bool : ats_false_bool) ;
> } // end of [atslib_eq_dev_dev]
> 
> ```
> 
> Line #72 is the one with “return (x1 == x2 ? ats\_true\_bool :  
> ats\_false\_bool) ;”
> 
> I’m surprised with this one: is there a case where C99 disallow a  
> comparison between two value of the same type? (here, `dev_t`).

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [January 31, 2015, 12:34pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/15 "2015-01-31T12:34:34Z")

</div>

> To clarify it, I meant the build of the tiny test file, not the build of  
> ATS2 (I will test it later).

Proceeding does not expose the previous error, but I get another one which  
I can’t figure how to solve.

I get this error: “/usr/include/asm-generic/int-ll64.h:19: syntax error.”

At /usr/include/asm-generic/int-ll64.h:19 , I have this:

```
 typedef __signed__ char __s8;

```

Side note: I noticed CompCert also returns syntax error on undefined types,  
but this does not seems to be the case here.

According to [The GNU C Reference Manual](http://www.gnu.org/software/gnu-c-manual/gnu-c-manual.html) ,  
` __signed__ ` is a GNU extension to C, so may be the headers must be told to  
conform to C99, may be defining another macro on the command line, but I  
don’t know which one. Some one who know GCC lib well have an idea?

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [January 31, 2015, 8:47pm UTC](https://discourse.ats-lang.org/t/trying-to-build-ats2-with-compcert/119/16 "2015-01-31T20:47:41Z")

</div>

> I’m stuck with a “syntax error” in `integer_fixed.cats` at line 58, the  
> line “typedef int64\_t atstype\_int64 ;”
> 
> As CompCert seems to complain about syntax error when it encounters an  
> undefined type, my guess is that it does not see the definition of the  
> `atstype_int64`.

Sorry, I meant it does not see a definition for `int64_t`. I wanted to go  
on, manually editing the file to change it into `long long`, but I have  
another error in “pointer.cats” at line 112. It complains “illegal pointer  
arithmetic in binary ‘-’ ”. The C source at that location is:

```
 ATSinline()
 atstype_ssize
 atspre_sub_ptr_ptr
   (atstype_ptr p1, atstype_ptr p2) { return (p1 - p2) ; }
 // end of [atspre_sub_ptr_ptr]
 #define atspre_sub_ptr0_ptr0 atspre_sub_ptr_ptr
 #define atspre_sub_ptr1_ptr1 atspre_sub_ptr_ptr

```

So it sees an issue with “return (p1 - p2) ;”

To be sure, I tried to compile this simple test file:

```
 #include <sys/types.h>

 typedef ssize_t atstype_ssize;
 typedef void* atstype_ptr;

 atstype_ssize
 atspre_sub_ptr_ptr
   (atstype_ptr p1, atstype_ptr p2) { return (p1 - p2) ; }
 // end of [atspre_sub_ptr_ptr]

```

And it complains the same, that is “test.c:8: Error: illegal pointer  
arithmetic in binary ‘-’.”

GCC does not complain with this test file.