AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification
Apache License 2.0
79 stars 14 forks source link

Add an attribute to rename definitions in the backend #237

Closed EschericHya closed 3 months ago

EschericHya commented 3 months ago

Fixes https://github.com/AeneasVerif/charon/issues/207

Still need to write some tests I guess

sonmarcho commented 3 months ago

Put aside the cleanup above, I would like to replace the Span field of Field with ItemMeta so that we can collect the attributes given to structure fields (and potentially rename fields).

Nadrieril commented 3 months ago

hm, if we use ItemMeta for things that aren't items then we shouldn't call it that

R1kM commented 3 months ago

I'd be in favour of wrapping up and merging this, and discussing the further extension to fields (and the precise name) in a further issue/PR. Wdyt?

sonmarcho commented 3 months ago

I just realized that we should also add some ItemMeta data to enumeration variants (similar to fields).

Nadrieril commented 3 months ago

Beware: another PR updated the Cargo.toml version, so when you merge main you'll have to update it again.

EDIT: I just added a CI check that should help us avoid this mistake.