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

Propagate target attribute #41

Closed karthikbhargavan closed 3 months ago

karthikbhargavan commented 3 months ago

This PR propagates target attributes to the C code. In particular, if you add to the config.yaml file:

- name: libcrux_sha3_avx2
   target: "avx2"
   ...

Then the file libcrux_sha3_avx2.c will contain:

KRML_ATTRIBUTE_TARGET("avx2")

before every function in the file.

This has only been tested on libcrux, so it may need a local test file and documentation.