generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 130
Closed
Labels
Z-ContractsIssue related to code contractsIssue related to code contracts[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.
Description
parse_stubs
uses resolve_fn_path
to resolve the target of the stub:
kani/kani-compiler/src/kani_middle/attributes.rs
Lines 859 to 862 in e229b69
fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<Stub> { | |
let current_module = tcx.parent_module_from_def_id(harness.expect_local()); | |
let check_resolve = |attr: &Attribute, path: &TypePath| { | |
let result = resolve_fn_path(tcx, current_module.to_local_def_id(), path); |
while interpret_for_contract_attribute
calls resolve_mod
,
kani/kani-compiler/src/kani_middle/attributes.rs
Lines 246 to 249 in e229b69
pub(crate) fn interpret_for_contract_attribute(&self) -> Option<(Symbol, DefId, Span)> { | |
self.expect_maybe_one(KaniAttributeKind::ProofForContract).and_then(|target| { | |
let name = expect_key_string_value(self.tcx.sess, target).ok()?; | |
self.resolve_from_mod(name.as_str()) |
which calls resolve_fn
instead
kani/kani-compiler/src/kani_middle/attributes.rs
Lines 335 to 340 in cc367b3
fn resolve_from_mod(&self, path_str: &str) -> Result<DefId, ResolveError<'tcx>> { | |
resolve_fn( | |
self.tcx, | |
self.tcx.parent_module_from_def_id(self.item.expect_local()).to_local_def_id(), | |
path_str, | |
) |
Investigate why this discrepancy exists and if alleviating it would let users write contracts for more kinds of functions. (See #4051 for context on this issue).
Metadata
Metadata
Assignees
Labels
Z-ContractsIssue related to code contractsIssue related to code contracts[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.