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
21 stars 1 forks source link

Drop core_num__u32_8__BITS eurydice_glue.h #3

Closed franziskuskiefer closed 8 months ago

franziskuskiefer commented 8 months ago

Drop core_num__u32_8__BITS. It doesn't work. It needs to be #defined in the header file manually for now.

msprotz commented 8 months ago

The generated code will contain a static inline without an initial value, which is just as unsafe. I instead fixed it with a hardcoded definition in 04c774a which now gives (in internal/core.h): 

#define CORE_NUM__U32_8__BITS (32U)
msprotz commented 8 months ago

This temporary fix will be revisited once we have support for passing a set of definitions from external crates to be extracted.

franziskuskiefer commented 8 months ago

@msprotz but we still have the static in the glue header.

msprotz commented 8 months ago

Ah yes I thought I had incorporated this, sorry.

msprotz commented 8 months ago

(This is now merged.)