rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
53 stars 28 forks source link

[CN] illegal combination of type specifiers #280

Closed podhrmic closed 6 days ago

podhrmic commented 5 months ago

CN throws this error referring to its own header file:

/root/.opam/default/lib/cerberus/runtime/libc/include/stdlib.h:26:1: error: constraint violation: illegal combination of type specifiers
long double strtold(const char * restrict nptr, char ** restrict endptr);
^~~~~~~~~~~~~~~~~~~~~~~ 
kmemarian commented 5 months ago

Do you also get the error with cerberus? Can would provide a translation unit causing the issue?

podhrmic commented 5 months ago

Looks like #include <stdlib.h> triggers this error in CN. # cerberus -I src/include --include=src/include/wars.h src/common.c returns 0.

Here is the source file triggering the error: https://github.com/GaloisInc/VERSE-OpenSUT/blob/main/components/mission_protection_system/src/common.c#L19

kmemarian commented 5 months ago

the issue comes from the following definition in wars.h:

#define double unsigned long long

which doesn't work for occurences of long double.

Btw, macro define named like a keyword are UB when they precede the include of a standard header (C11 §7.1.2#4).