polonius

이는 대출 수표를 모델링하는 핵심 라이브러리입니다. 이는 이 블로그 게시물과 이 강연에 설명된 분석을 구현합니다. 자세한 내용은 Polonius 책에 나와 있습니다.

왜 이름이 "폴로니우스"입니까?

이 이름은 셰익스피어의 햄릿 에 등장하는 폴로니우스(Polonius)의 유명한 인용문 "빌리는 사람도, 빌려주는 사람도 아니다"에서 유래되었습니다.

코드를 실행하시겠습니까?

이 저장소의 목표 중 하나는 동일한 알고리즘의 다양한 구현을 실험하고 비교하는 것입니다. cargo run 사용하여 분석을 실행할 수 있으며 -a 사용하여 분석을 선택할 수 있습니다. 예를 들어 박수에서 추출한 예제에 대해 실행하려면 다음을 수행할 수 있습니다.

 > cargo +nightly run --release -- -a DatafrogOpt inputs/clap-rs/app-parser-{{impl}}-add_defaults/
    Finished release [optimized] target(s) in 0.05 secs
     Running ` target/release/borrow-check ' inputs/clap-rs/app-parser-{{impl}}-add_defaults/ ' `
--------------------------------------------------
Directory: inputs/clap-rs/app-parser-{{impl}}-add_defaults/
Time: 3.856s

-a Naive 시도하여 순진한 규칙(더 읽기 쉽고 느림)을 얻을 수도 있습니다. 이는 블로그 게시물에 설명된 정확한 규칙입니다. -a LocationInsensitive 사용하여 위치를 구분하지 않는 분석을 사용할 수도 있습니다(더 빠르지만 가짜 오류가 발생할 수 있음).

기본적으로 cargo run 타이밍만 인쇄합니다. 결과도 보려면 --show-tuples (오류 표시) 및 -v (더 많은 중간 계산 표시)를 시도하세요. --help 제공하여 더 많은 문서를 얻을 수 있습니다.

자신만의 입력을 생성하는 방법

입력에 대해 빌림 검사기를 실행하려면 먼저 입력 사실을 생성해야 합니다. 이를 위해서는 -Znll-facts 옵션을 사용하여 Rustc를 실행해야 합니다:

 > rustc -Znll-facts inputs/issue-47680/issue-47680.rs

또는 #![feature(nll)] 플래그를 사용하여 크레이트의 입력 사실을 생성하려면:

 > cargo rustc -- -Znll-facts

그러면 함수당 하나의 하위 디렉터리가 있는 nll-facts 디렉터리가 생성됩니다.

 > ls -F nll-facts
{{impl}}-maybe_next/  main/

그런 다음 이 디렉터리에서 실행할 수 있습니다.