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

Static loop unrolling fails if loop body contains a struct #19

Open msprotz opened 4 months ago

msprotz commented 4 months ago

See commit fcc0213 which works around the issue.

Basically, if a struct is used in the loop body, then it generates a compound literal that contains a comma, and then the preprocessor thinks that the macro KRML_MAYBE_UNROLL(..., <>) receives too many arguments.

From https://stackoverflow.com/questions/13842468/comma-in-c-c-macro#19841470, which is moderately useful, two solutions are:

The former seems easier to implement