always_inline seems to also require inline

FStarLang / karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code

Apache License 2.0

394 stars 58 forks source link

always_inline seems to also require inline #444

Closed karthikbhargavan closed 2 months ago

karthikbhargavan commented 2 months ago

When adding __attribute((always_inline)) to a function, the compiler complains if it is not also marked with inline. This PR changes the KRML_MUSTINLINE macro to always add inline as well.