A stable identifier should be produced to identify each exported/serialized spec:
If we want to use sth in hir level (likely a crate_id or hash of it), since we are accessing the tokenstream and edit it, at the time when we want to do the reading, we don't have any info available to us. That is, the reading happens at the syntax tree level, we don't have access to the hir thing there yet
The alternative is to use a hash of the file's path, the difficulty is to resolve the path for the file we are calling prusti on, since we need that when we try to write serialized spec into disk. (i.e. if I have #[extern_spec] in crate::main.rs, how do I get that path in the syntax level?
We may want to include cargo crate? That can provide us with more info
3
A stable identifier should be produced to identify each exported/serialized spec:
hirlevel (likely a crate_id or hash of it), since we are accessing the tokenstream and edit it, at the time when we want to do the reading, we don't have any info available to us. That is, the reading happens at the syntax tree level, we don't have access to thehirthing there yet#[extern_spec]in crate::main.rs, how do I get that path in the syntax level?