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

Propagate inline attributes #40

Closed karthikbhargavan closed 1 month ago

karthikbhargavan commented 1 month ago

This PR improves the treatment of inline attributes in Rust.

The last of these is security-critical for constant-time code. There is an example of these usages in test/inline_attributes