Function emit_verify_summary 

fn emit_verify_summary<'tcx>(
    tcx: TyCtxt<'tcx>,
    target_path: &str,
    def_id: DefId,
    all_results: &[PropertyCheckResult<'tcx>],
    mode: VerifyMode,
)