search

AeneasVerif / eurydice

Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.
Apache License 2.0
22 stars 1 forks source link

Include krmllib.h in eurydice_glue.h #2

Closed franziskuskiefer closed 10 months ago

franziskuskiefer commented 10 months ago

Can we include krmllib.h instead in the glue? This breaks tests here like this because the include is missing. But adding the include path should fix that.

wdyt?

msprotz commented 10 months ago

Including the whole of krmllib.h is a little heavy-handed. I would just include this for now: https://github.com/FStarLang/karamel/blob/master/include/krml/lowstar_endianness.h

thoughts?

franziskuskiefer commented 10 months ago

Yeah I think that should be enough. Let me test it

franziskuskiefer commented 10 months ago

This should work. But the tests fail for me. Because of the macro changes. But they fail on main too because of that.