We previously introduced type_map.json and restrictions.json as output files from rmc-rustc. And now for proof harnesses (and more) we have rmc-metadata.json.
We should merge the above two into rmc-metadata.json.
In the end, we'll just have:
symtab.json for cbmc's consumption.
rmc-metadata.json for consumption by our tools, which contains everything else we want to know.
As part of this, we should have a crate use to serialize/deserialize this format. Currently, this is mixed around in a few different places:
compiler/rustc_codegen_rmc/src/context/metadata.rs
library/rmc_restrictions/
We should create an rmc_metadata crate to house all these schemas.
We previously introduced
type_map.jsonandrestrictions.jsonas output files fromrmc-rustc. And now for proof harnesses (and more) we havermc-metadata.json.We should merge the above two into
rmc-metadata.json.In the end, we'll just have:
symtab.jsonfor cbmc's consumption.rmc-metadata.jsonfor consumption by our tools, which contains everything else we want to know.As part of this, we should have a crate use to serialize/deserialize this format. Currently, this is mixed around in a few different places:
compiler/rustc_codegen_rmc/src/context/metadata.rslibrary/rmc_restrictions/We should create an
rmc_metadatacrate to house all these schemas.