Skip to main content

get_std_contracts_from_json

rapx::verify::contract::json

Function get_std_contracts_from_json 

Source 
pub(crate) fn get_std_contracts_from_json(
    tcx: TyCtxt<'_>,
    def_id: DefId,
) -> Option<&'static [JsonProperty]>
Expand description

Looks up backup contracts for a standard-library function by its normalized path. For trait-method impls, resolves to the trait method’s path first so that all impls share the same contracts.

After exact-path lookup, first strips impl-block type segments, then falls back to wildcard patterns by progressively replacing the tail segment with *. For example, for core::slice::<impl [T]>::as_chunks, the fallback chain is:

  1. core::slice::<impl [T]>::as_chunks (exact)
  2. core::slice::as_chunks (impl segments stripped)
  3. core::slice::<impl [T]>::* (all methods of [T])
  4. core::slice::* (all functions in slice module)
  5. core::* (anything in core crate)