AeneasVerif / charon

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

Use `Vector`s instead of `Generator`+`Map` pairs #240

Closed Nadrieril closed 3 months ago

Nadrieril commented 3 months ago

This is a small API improvement: instead of generating ids with Generator and storing them in a Map, this uses Vector to do both at once. I tweaked Vector to be able to reserve slots in advance (by storing None) and fill them later.

Long-term I'd like to ensure we always store a value for each id (potentially an explicit error value) to avoid surprises.