search

LDY1998 / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.ethz.ch
Other
0 stars 0 forks source link

Why visit twice? #1

Open LDY1998 opened 3 years ago

LDY1998 commented 3 years ago

The hir tree is visited twice in the process, mainly by the SpecCollector struct in SpecCollector and in CollectPrustiSpecVisitor

There are slight difference between 2 visitor where collect_visitor has visit item and the spec_collector call visit_fn for a couple of times

Aurel300 commented 3 years ago

CollectPrustiSpecVisitor only collects annotated procedures… I'm pretty sure SpecCollector already does basically this, in the keys of the returned DefSpecificationMap. We should eventually get rid of CollectPrustiSpecVisitor if we can.