cpachecker
1.0.0
더 많은 문서는 doc/ Directory에서 찾을 수 있습니다.
CPACHECKER는 Dirk Beyer 및 기타의 저작권을 가진 Apache 2.0 라이센스에 따라 라이센스를 부여받습니다 (모든 기여자의 전체 목록에 대한 저자 .md). 타사 라이브러리는 기타 다양한 라이센스 및 저작권에 따라 있습니다. 정식 라이센스 텍스트에 대한 디렉토리 LICENSES 의 파일. 특히 MathSAT는 연구 및 평가 목적으로 만 사용할 수 있습니다 ( LICENSES/LicenseRef-MathSAT-CPAchecker.txt ). 필요한 경우 다른 SMT 솔버를 사용해야합니다. GPL 프로그램은 cpachecker와 함께 배포되지만 Cpachecker는 해당 프로그램과 분리되어 GPL의 조건에 따라 다르지 않습니다.
모든 프로그램은 C 프리 프로세서와 사전 처리해야하며, 즉 #define 및 #include 지시문을 포함하지 않을 수 있습니다. 명령 줄에 --preprocess 지정하여 cpachecker 내부에서 사전 처리를 활성화 할 수 있습니다. 여러 C 파일을 제공 할 수 있으며 함께 연결되어 단일 프로그램 (실험 기능)으로 확인됩니다.
CPACHECKER는 (GNU)의 큰 부분 집합을 구문 분석하고 분석 할 수 있습니다. c. 프로그램에 구문 분석이 실패하면 [email protected]에 보고서를 보내십시오.
확인하려는 소스 코드 파일을 선택하십시오. 자신의 프로그램을 사용하는 경우 위에서 언급 한대로 사전 프로세스를하십시오. 예 : doc/examples/example.c 또는 doc/examples/example_bug.c 더 많은 예제 프로그램의 좋은 소스는 예를 들어 소프트웨어 검증에 대한 국제 경쟁에서 사용되는 SV-Benchmarks 저장소입니다.
선택적으로 : 술어 분석과 같은 특정 분석을 선택하려면 구성 파일을 지정하십시오. 이 파일은 예를 들어 어떤 CPA가 사용되는지 정의합니다. 표준 구성 파일은 디렉토리 config/ 에서 찾을 수 있습니다. 특정 분석을 원하지 않으면 CPACHECKER의 기본 구성을 권장합니다. 그러나 MACOS에있는 경우 기본 구성이 작동하도록 특별히 컴파일 된 MathSat Binaries를 제공해야합니다 (또는 CPACHECKER의 Linux 버전을 실행하려면 Docker를 사용하십시오). cpachecker의 구성은 doc/Configuration.md 에 설명되어 있습니다.
사양 파일을 선택하십시오 (일부 구성에는 필요하지 않을 수 있음). 표준 구성은 config/specification/default.spc 기본 사양으로 사용합니다. 이를 통해 CPACHECKER는 ERROR (CASE Insensitive)라는 레이블과 소스 코드 파일의 어설 션을 찾습니다. 사양에 대한 다른 예제는 cpachecker 디렉토리에서 config/specification/ 에서 찾을 수 있습니다.
bin/cpachecker [ --config <CONFIG_FILE> ] [ --spec <SPEC_FILE> ] <SOURCE_FILE> 추가 명령 줄 인수는 doc/Configuration.md 에 설명되어 있습니다. CPACHECKER의 기본 구성 bin/cpachecker doc/examples/example.c 사용하려면 소스 파일 만 전달하십시오. 예를 들어 bin/cpachecker --config/kInduction.properties doc/examples/example.c 또는 동등한 약어 bin/cpachecker --kInduction doc/examples/example.c 로 특정 분석 (예 : K- 유도)을 선택할 수 있습니다. Java 17 이상이 필요합니다. 경로에 있지 않은 경우 환경 변수 Java에 지정해야합니다. 예 : export JAVA=/usr/lib/jvm/java-17-openjdk-amd64/bin/java 는 Ubuntu에서 64bit OpenJDK 17입니다.
이 플랫폼 용 SMT 솔버 용 바이너리를 배송하지 않기 때문에 모든 분석 구성을 MACOS에 사용할 수있는 것은 아닙니다. 적절한 바이너리를 직접 구축하거나 Java 기반 솔버와 함께 작동하는 덜 강력한 분석을 사용해야합니다. 예를 들어 Cpachecker의 기본 구성 대신 --predicateAnalysis-linear --option solver.solver=SMTInterpol 도 CPACHECKER의 Linux 버전을 실행하는 데 Docker와 같은 솔루션을 사용할 수도 있습니다.
Docker를 사용하여 CPACHECKER를 설치 한 경우 위의 사령부는 다음과 같습니다. docker run -v $(pwd):/workdir -u $UID:$GID sosylab/cpachecker /cpachecker/doc/examples/example.c 현재 디렉토리가 현재 디렉토리를 제공하여 현재 디렉토리를 제공합니다. CPACHECKER. cpachecker의 출력 파일은 ./output/ 에 배치됩니다.
콘솔 출력에 추가로 대화식 HTML 보고서는 디렉토리 output/ , Report.html (결과의 경우) 또는 Counterexample.*.html (결과 false)에서 생성됩니다. CPACHECKER 분석 결과를보기 위해 브라우저 doc/Report.md 이러한 파일을 열어
디렉토리 output/ 에 추가 출력 파일도 있습니다.
ARG.dot : 초록 도달성 트리의 시각화 (GraphViz 형식)cfa*.dot : 제어 흐름의 시각화 (GraphViz 형식)reached.dot : 도트 : 제어 흐름의 시각화가 상단에 시각화 된 추상 상태와 함께 (GraphViz 형식)coverage.info : Gcov 형식의 적용 범위 정보 (테스트 도구와 유사) 다음 명령 줄을 사용하여 HTML 보고서를 output/index.html : genhtml output/coverage.info --output-directory output --legend 로 생성합니다.Counterexample.*.txt : 오류로 이어지는 프로그램을 통한 경로Counterexample.*.assignment.txt : 오류 경로의 모든 변수에 대한 할당.Counterexample.*.harness.c : 테스트 실행을 통해 오류 경로를 재현 할 수있는 테스트 하네스. 예제 사용은 Doc/Tutorials/Test-Harness.md를 참조하십시오.predmap.txt : 프로그램 안전을 증명하기 위해 술어 분석에서 사용하는 사전.reached.txt : txt : 모든 초록 상태에 도달 한 모든 덤프Statistics.txt : 시간 통계 ( --stats 사용하여 콘솔에도 인쇄 할 수 있음)이러한 모든 파일이 모든 구성에 사용할 수있는 것은 아닙니다. 또한 이러한 파일 중 일부는 오류가 발견 된 경우에만 생성됩니다 (또는 그 반대로). Cpachecker는이 디렉토리에서 파일을 덮어 씁니다!
CPACHECKER의 일부인 CPA-Witness2Test로 위반 증인을 검증 할 수 있습니다.
그렇게하려면 위반 증인, 위반 증인에 맞는 사양 파일 및 위반 증인에 맞는 소스 코드 파일이 필요합니다.
증인을 검증하려면 다음 명령을 실행하십시오.
bin/cpa-witness2test --witness <WITNESS_FILE> --spec <SPEC_FILE> <SOURCE_FILE>`
추가 명령 줄 인수는 bin/cpa-witness2test -h 로 볼 수 있습니다.
완료되면 위반 증인이 성공적으로 검증되면 콘솔 출력은 Verification result: FALSE . CPA-Witness2Test는 콘솔 출력에 추가로 파일 output/*.harness.c 만듭니다. 이 파일은 소스 파일에 대해 컴파일하여 위반 증인을 반영하는 실행 가능한 테스트를 생성 할 수 있습니다.
위반 증인이 실행 가능한 테스트를 만들기에 충분한 정보를 포함하지 않으면 유효성 검사 결과는 ERROR 이며 콘솔 출력에는 다음 줄이 포함됩니다. Could not export a test harness, some test-vector values are missing.
