가능한 값을 추상화하기
프로그램을 실제 입력마다 실행하기보다 값과 상태의 범위를 추상적으로 계산한다. 제어 흐름과 고정점 계산 및 수치 추상 도메인 같은 구성 요소를 사용한다. 분석의 정밀도와 확장성은 선택한 추상화와 설정에 영향을 받는다. 확인할 오류 종류와 진입점 및 외부 입력 가정을 분명히 한다.
보고 상태를 구분하기
보고서는 안전하다고 확인한 지점과 오류 및 도달하지 않는 지점과 경고를 나누어 보여 준다. 경고는 일부 실행에서 오류가 가능하거나 정보가 부족하거나 분석이 충분히 정밀하지 않은 경우를 포함할 수 있다. 따라서 모든 경고를 실제 오류로 단정하거나 전부 무시하지 않고 발생 조건을 조사한다.
결과와 실행 환경
분석 결과를 데이터베이스에 기록하고 터미널이나 웹 인터페이스로 살펴볼 수 있다. 프로그램의 소스와 bitcode가 같은 버전을 나타내는지 확인하고 LLVM 및 Clang의 지원 구성을 맞춘다. 분석 라이브러리와 특정 언어의 분석기는 다른 역할을 한다. 선택한 검사 성질에서의 안전 결과를 구현의 모든 업무 규칙이나 운영 환경까지 보장하는 결과로 확대하지 않는다.
관련 문서
CPAchecker / SeaHorn / Symbiotic / Frama-C