Skip to main content

taint_paths

logicaffeine_kernel::interface::lean::taint

Function taint_paths 

Source 
pub fn taint_paths(
    imported: &ImportedContext,
    target: &str,
    assumptions: &[String],
) -> Vec<TaintPath>
Expand description

The taint path of each of assumptions (Lean names) from target (a kernel name), in the order assumptions lists them. An assumption the target does not reach through the environment has no path and is left out.