File tree Expand file tree Collapse file tree 4 files changed +5
-5
lines changed
kani-compiler/src/kani_middle Expand file tree Collapse file tree 4 files changed +5
-5
lines changed Original file line number Diff line number Diff line change @@ -691,7 +691,7 @@ impl<'tcx> KaniAttributes<'tcx> {
691691 if !generics. own_params . is_empty ( ) {
692692 err = err. with_help (
693693 "Kani does not currently support stubs or function contracts on generic functions in traits.\n \
694- See <ISSUE LINK> for more information.",
694+ See https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734 for more information.",
695695 ) ;
696696 }
697697 }
Original file line number Diff line number Diff line change @@ -696,7 +696,7 @@ fn resolve_in_trait_def_stable<'tcx>(
696696}
697697
698698/// Resolves a function in a trait definition.
699- /// TODO: remove this function in favor of `resolve_in_trait_def_stable`, c.f. <ISSUE LINK>
699+ /// TODO: remove this function in favor of `resolve_in_trait_def_stable`, c.f. https://github.com/model-checking/kani/issues/4252
700700fn resolve_in_trait_def < ' tcx > (
701701 tcx : TyCtxt < ' tcx > ,
702702 trait_id : DefId ,
Original file line number Diff line number Diff line change @@ -5,7 +5,7 @@ generic_trait_fn.rs\
55| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
66|\
77 = help: Kani does not currently support stubs or function contracts on generic functions in traits.\
8- See <ISSUE LINK> for more information.
8+ See https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734 for more information.
99
1010error: failed to resolve `<TestStruct as TraitY>::generic_fn`: unable to find implementation of associated function `TraitY::generic_fn` for TestStruct\
1111generic_trait_fn.rs\
@@ -14,6 +14,6 @@ generic_trait_fn.rs\
1414| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
1515|\
1616 = help: Kani does not currently support stubs or function contracts on generic functions in traits.\
17- See <ISSUE LINK> for more information.
17+ See https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734 for more information.
1818
1919error: aborting due to 2 previous errors
Original file line number Diff line number Diff line change 44// kani-flags: --harness harness -Z stubbing
55// This stub should work, since the function signatures are identical,
66// but we do not yet support stubbing/contracts on trait fns with generic arguments
7- // c.f. <ISSUE LINK> .
7+ // c.f. https://github.com/model-checking/kani/issues/1997#issuecomment-3134614734 .
88// For now, test that we emit a nice error message.
99
1010trait TraitX {
You can’t perform that action at this time.
0 commit comments