Separate compilation with -static-header -library does not honor CMacro
tahina-pro opened this issue · 1 comments
tahina-pro commented
On https://github.com/FStarLang/kremlin/tree/taramana_sepcomp_cmacro/test/sepcomp
a
contains a library:
A.Base
contains definitions that are extracted toA.h
withstatic inline
s and a macroA_THIS_IS_A_CONSTANT
, as expectedA.Combinators
contains a higher-order functionf
that is not extracted, as expected. That functionf
usesA_THIS_IS_A_CONSTANT
.
b
contains an application that uses A.Combinators.f
without extracting A.h
again. Thus, b
is indirectly using A.Base.this_is_a_constant
declared as CMacro
, but I end up with B.h
declaring and B.c
using A_this_is_a_constant
, instead of the expected A_THIS_IS_A_CONSTANT
from A.h
tahina-pro commented
Thank you @msprotz for having fixed this bug! Just merged into master
.